aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eqschemes.ml')
-rw-r--r--tactics/eqschemes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index ce57682c6..bfbac7787 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -64,7 +64,7 @@ module RelDecl = Context.Rel.Declaration
let hid = Id.of_string "H"
let xid = Id.of_string "X"
let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
-let fresh env id = next_global_ident_away id []
+let fresh env id = next_global_ident_away id Id.Set.empty
let with_context_set ctx (b, ctx') =
(b, Univ.ContextSet.union ctx ctx')