Commit 8f217412 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Removed the extraction directive from Locations, since we don't extract.

parent 12305b37
......@@ -13,7 +13,7 @@ Require Import Coq.Sorting.Mergesort.
*)
Module Type Locations.
Parameter Inline(10) t : Set.
Parameter t : Set.
Parameter eq_dec : forall x y : t, {x = y} + {x <> y}.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment