First version of refine for MutCase, still largely incomplete.

[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 24a94514e8703dd5ca92d7feb526bbf31930fd80..0ee364053f846667059467ec1dc7ac44afe73cb5 100644 (file)
--- 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)