sort metavariables are now generated in an empty canonical context.

[helm.git] / helm / ocaml / cic_unification / cicMkImplicit.ml

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 99e599ab2f6feff6e9bcfe4ce8d6a3d21fe3a3c6..fc429b381e1c393b23f6190b5c84a904410e9fcc 100644 (file)
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -28,8 +28,8 @@ let new_meta metasenv =
 let mk_implicit metasenv context =
   let newmeta = new_meta metasenv in
   let irl = identity_relocation_list_for_metavariable context in
-  ([ newmeta, context, Cic.Sort Cic.Type ;
-    newmeta + 1, context, Cic.Meta (newmeta, irl);
+  ([ newmeta, [], Cic.Sort Cic.Type ;
+    newmeta + 1, context, Cic.Meta (newmeta, []);
     newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
    newmeta + 2)
 
@@ -63,9 +63,8 @@ let fresh_subst metasenv context uris =
 
 let mk_implicit_type metasenv context =
   let newmeta = new_meta metasenv in
-  let irl = identity_relocation_list_for_metavariable context in
-  ([ newmeta, context, Cic.Sort Cic.Type ;
-    newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv,
+  ([ newmeta, [], Cic.Sort Cic.Type ;
+    newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
    newmeta + 1)
 
 let expand_implicits metasenv context term =