From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Feb 2004 18:06:28 +0000 (+0000)
Subject: sort metavariables are now generated in an empty canonical context.
X-Git-Tag: V_0_2_3~12
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6fe855a9ae94552950eaa7f1d5e926ffdd463131;p=helm.git

sort metavariables are now generated in an empty canonical context.
---

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 99e599ab2..fc429b381 100644
--- 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 =