- tacticals: new tactical ifs added: uses thens where if_ uses then_

[helm.git] / components / tactics / proofEngineHelpers.ml

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index b5db34d17c8b852bdd2ca9988f10dd46feb4ed0b..246751b32785f52b49cad40cff47f7172fffe469 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -707,3 +707,19 @@ let sort_metasenv (m : Cic.metasenv) =
   (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
 ;;
   
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+  * names as long as they are available, then it fallbacks to name generation
+  * using FreshNamesGenerator module *)
+let namer_of names =
+  let len = List.length names in
+  let count = ref 0 in
+  fun metasenv context name ~typ ->
+    if !count < len then begin
+      let name = match List.nth names !count with
+         | Some s -> Cic.Name s
+        | None   -> Cic.Anonymous
+      in
+      incr count;
+      name
+    end else
+      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ