X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.ml;h=0ee364053f846667059467ec1dc7ac44afe73cb5;hb=6d9de12a536ee4b9e369849ff7e9aa4ca464de9d;hp=24a94514e8703dd5ca92d7feb526bbf31930fd80;hpb=103c147d078e431ee0bfc7393715f0db34dfdd8d;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 24a94514e..0ee364053 100644
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -33,6 +33,34 @@ let mk_implicit metasenv context =
     newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
    newmeta + 2)
 
+let n_fresh_metas metasenv context n = 
+  if n = 0 then metasenv, []
+  else 
+    let irl = identity_relocation_list_for_metavariable context in
+    let newmeta = new_meta metasenv in
+    let rec aux newmeta n = 
+      if n = 0 then metasenv, [] 
+      else
+        let metasenv', l = aux (newmeta + 3) (n-1) in 
+        (newmeta, context, Cic.Sort Cic.Type)::
+        (newmeta + 1, context, Cic.Meta (newmeta, irl))::
+        (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
+        Cic.Meta(newmeta+2,irl)::l in
+    aux newmeta n
+      
+let fresh_subst metasenv context uris = 
+  let irl = identity_relocation_list_for_metavariable context in
+  let newmeta = new_meta metasenv in
+  let rec aux newmeta = function
+      [] -> metasenv, [] 
+    | uri::tl ->
+       let metasenv', l = aux (newmeta + 3) tl in 
+         (newmeta, context, Cic.Sort Cic.Type)::
+         (newmeta + 1, context, Cic.Meta (newmeta, irl))::
+         (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
+          (uri,Cic.Meta(newmeta+2,irl))::l in
+    aux newmeta uris
+
 let mk_implicit' metasenv context =
   let (metasenv, index) = mk_implicit metasenv context in
   (metasenv, index - 1, index)