fresh_name_generator has now also the metasenv parameter.

Before this patch it used the empty metasenv (and it worked, somehow!)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 81f9acd666ed8be82a217d2cc6aa56f7ff4d3a3d..b62f4b6245dbc5b88b73df47bc8ab77633277f49 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -556,9 +556,9 @@ let decompose_uris_choice_callback uris =
     ) 
 ;;
 
-let mk_fresh_name_callback context name ~typ =
+let mk_fresh_name_callback metasenv context name ~typ =
  let fresh_name =
-  match FreshNamesGenerator.mk_fresh_name context name ~typ with
+  match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with
      Cic.Name fresh_name -> fresh_name
    | Cic.Anonymous -> assert false
  in

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index e4a9fa2e96d8cf991a64a4ee0641093242735821..2b0e58d214328d4a7e7c18b5600658a9ac4e283f 100644 (file)
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -62,8 +62,7 @@ module type Callbacks =
     val decompose_uris_choice_callback :
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
-    val mk_fresh_name_callback :
-      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
   end
 ;;
 

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 200e50a15535eb69da4044fbc7f766eab9399e0c..a304e7e3b27efb8005e32f0cd3e96bacc7ddb7ba 100644 (file)
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -60,8 +60,7 @@ module type Callbacks =
     val decompose_uris_choice_callback :
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
-    val mk_fresh_name_callback :
-      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
   end
 
 module type Tactics =

diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend
index eb500c9210e43c5580a958a6ec6ab4e41dc4ed53..8828b40df3b0295396ecaf9d68b0ac1acb51ea0c 100644 (file)
--- a/helm/ocaml/cic_unification/.depend
+++ b/helm/ocaml/cic_unification/.depend
@@ -8,6 +8,6 @@ cicMetaSubst.cmx: cicMetaSubst.cmi
 cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi 
 cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi 
 cicRefine.cmo: cicMetaSubst.cmi cicMkImplicit.cmi cicUnification.cmi \
-    cicRefine.cmi 
+    freshNamesGenerator.cmi cicRefine.cmi 
 cicRefine.cmx: cicMetaSubst.cmx cicMkImplicit.cmx cicUnification.cmx \
-    cicRefine.cmi 
+    freshNamesGenerator.cmx cicRefine.cmi 

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 3f0006a39cf285da71a580ffa57f37b66f1ea87c..3f4d777c9f2d3164742932d691e151b3c60f7da2 100644 (file)
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -27,14 +27,14 @@
 (* returns an identifier which is fresh in the context *)
 (* and that resembles [name] as much as possible.      *)
 (* [typ] will be the type of the variable              *)
-let mk_fresh_name context name ~typ =
+let mk_fresh_name metasenv context name ~typ =
  let module C = Cic in
   let basename =
    match name with
       C.Anonymous ->
        (*CSC: great space for improvements here *)
        (try
-         (match CicTypeChecker.type_of_aux' [] context typ with
+         (match CicTypeChecker.type_of_aux' metasenv context typ with
              C.Sort C.Prop
            | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli
index e350363e9d7e624d15a7cc96fed72c5ad07078d2..371ca99fa323e31d1873df3c68b843ef4f135989 100644 (file)
--- a/helm/ocaml/cic_unification/freshNamesGenerator.mli
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli
@@ -23,8 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* mk_fresh_name context name typ                      *)
+(* mk_fresh_name metasenv context name typ             *)
 (* returns an identifier which is fresh in the context *)
 (* and that resembles [name] as much as possible.      *)
 (* [typ] will be the type of the variable              *)
-val mk_fresh_name : Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+val mk_fresh_name :
+ Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 304f10450fadd1585d4b5b9fea275801c82abe55..ac28f9a28e225d36c1dff3f9328d916bef36f250 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -59,7 +59,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
-       (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'')
+       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+         ty, gty'')
     in
     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
     let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
@@ -120,7 +121,8 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
-       (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'')
+       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+         ty, gty'')
     in
     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
     let irl =

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 2b505b79de725cdb87974c4d4d8622d3773f7fb6..a518edaa67193486f259b643bdcc387a90a49798 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -37,13 +37,13 @@ exception WrongUriToVariable of string
 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
 (* So, lambda_abstract is the core of the implementation of *)
 (* the Intros tactic.                                       *)
-let lambda_abstract context newmeta ty mk_fresh_name =
+let lambda_abstract metasenv context newmeta ty mk_fresh_name =
  let module C = Cic in
   let rec collect_context context =
    function
       C.Cast (te,_)   -> collect_context context te
     | C.Prod (n,s,t)  ->
-       let n' = mk_fresh_name context n ~typ:s in
+       let n' = mk_fresh_name metasenv context n ~typ:s in
         let (context',ty,bo) =
          collect_context ((Some (n',(C.Decl s)))::context) t
         in
@@ -115,7 +115,8 @@ let eta_expand metasenv context t arg =
     T.type_of_aux' metasenv context arg
    in
     let fresh_name =
-     FreshNamesGenerator.mk_fresh_name context (Cic.Name "Heta") ~typ:argty
+     FreshNamesGenerator.mk_fresh_name
+      metasenv context (Cic.Name "Heta") ~typ:argty
     in
      (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg])
 
@@ -321,7 +322,7 @@ let intros_tac
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let newmeta = new_meta_of_proof ~proof in
     let (context',ty',bo') =
-     lambda_abstract context newmeta ty mk_fresh_name_callback
+     lambda_abstract metasenv context newmeta ty mk_fresh_name_callback
     in
      let (newproof, _) =
        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
@@ -338,7 +339,7 @@ let cut_tac
    let newmeta1 = new_meta_of_proof ~proof in
    let newmeta2 = newmeta1 + 1 in
    let fresh_name =
-    mk_fresh_name_callback context (Cic.Name "Hcut") ~typ:term in
+    mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
    let context_for_newmeta1 =
     (Some (fresh_name,C.Decl term))::context in
    let irl1 =
@@ -370,7 +371,7 @@ let letin_tac
    let _ = CicTypeChecker.type_of_aux' metasenv context term in
     let newmeta = new_meta_of_proof ~proof in
     let fresh_name =
-     mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in
+     mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
     let context_for_newmeta =
      (Some (fresh_name,C.Def (term,None)))::context in
     let irl =

diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml
index 178be54d441a6e16ef01b3d6ec876be3ff974da9..334c594da4b9d7d5564d5305825d463b83736e7d 100644 (file)
--- a/helm/ocaml/tactics/proofEngineTypes.ml
+++ b/helm/ocaml/tactics/proofEngineTypes.ml
@@ -42,4 +42,4 @@ exception Fail of string
 
   (** constraint: the returned value will always be constructed by Cic.Name **)
 type mk_fresh_name_type =
- Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+ Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 28acd57ec250400b5144b5098999b68cca72e412..64b9ff790618c6305938d685229ecbb73c6801be 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -83,7 +83,7 @@ let generalize_tac
       ~start:
         (P.cut_tac 
          (C.Prod(
-           (mk_fresh_name_callback context C.Anonymous typ), 
+           (mk_fresh_name_callback metasenv context C.Anonymous typ), 
            typ,
            (ProofEngineReduction.replace_lifting_csc 1
              ~equality:(==)