Typing of intros_tac improved. It now has a parameter that is a fresh-names

generator.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 07a94a9b1252108ffed55b294fef0447eab75d3d..c08183bebf889300aa8c56893930d4a842e3deaf 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -1002,7 +1002,9 @@ let assumption_tac ~status:(proof,goal)=
 (* !!!!! fix !!!!!!!!!! *)
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
-               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
+                (*inutile sia questo che quello prima  della chiamata*)
+               ~start:
+                  (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
                ~continuation:(Tacticals.then_ 
                        ~start:(VariousTactics.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
@@ -1044,7 +1046,8 @@ theoreme,so let's parse our thesis *)
 
    let proof,gl = Tacticals.then_ 
        ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-       ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
+       ~continuation:
+          (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
                ~status:(s_proof,s_goal) in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 8b3f025aa07a575e9e9015528010d725b9bee5f7..eba2d571ff8d4fc26ed633f375f3be1fd89872cd 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -37,7 +37,7 @@ 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 name =
+let lambda_abstract context newmeta ty mknames =
  let module C = Cic in
   let rec collect_context context =
    function
@@ -46,8 +46,7 @@ let lambda_abstract context newmeta ty name =
        let n' =
         match n with
            C.Name _ -> n
-(*CSC: generatore di nomi? Chiedere il nome? *)
-         | C.Anonymous -> C.Name name
+         | C.Anonymous -> C.Name (mknames ())
        in
         let (context',ty,bo) =
          collect_context ((Some (n',(C.Decl s)))::context) t
@@ -306,13 +305,13 @@ let apply_tac ~term ~status =
   with CicUnification.UnificationFailed as e ->
     raise (Fail (Printexc.to_string e))
 
-let intros_tac ~name ~status:(proof, goal) =
+let intros_tac ~mknames ~status:(proof, goal) =
  let module C = Cic in
  let module R = CicReduction in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let newmeta = new_meta ~proof in
-    let (context',ty',bo') = lambda_abstract context newmeta ty name in
+    let (context',ty',bo') = lambda_abstract context newmeta ty mknames in
      let (newproof, _) =
        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
      in
@@ -508,7 +507,7 @@ let elim_simpl_intros_tac ~term =
   ~continuation:
    (Tacticals.then_
      ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
-     ~continuation:(intros_tac ~name:"FOO"))
+     ~continuation:(intros_tac ~mknames:(function () -> "FOO")))
 ;;
 
 

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index b23e4005fa7e6a7216017c8bb4ed206e3bf9b3ab..1fa97805ac50356a407448f5ca206c0a55fecd2b 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.mli
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -28,7 +28,7 @@ val apply_tac:
 val exact_tac:
   term: Cic.term -> ProofEngineTypes.tactic
 val intros_tac:
-  name: string -> ProofEngineTypes.tactic
+  mknames: (unit -> string) -> ProofEngineTypes.tactic
 val cut_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 val letin_tac:

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index dbf04c393386c0d57e5e74faf57ec4e9b242092f..173c1c59d3195f374fe087513c8d188d411d9855 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -138,11 +138,10 @@ let perforate context term ty =
 
 (*CSC: generatore di nomi? Chiedere il nome? *)
 let fresh_name =
- let next_fresh_index = ref 0
-in
- function () ->
-  incr next_fresh_index ;
-  "fresh_name" ^ string_of_int !next_fresh_index
+ let next_fresh_index = ref 0 in
+  function () ->
+   incr next_fresh_index ;
+   "fresh_name" ^ string_of_int !next_fresh_index
 
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 let reduction_tactic_in_scratch reduction_function term ty =
@@ -174,7 +173,7 @@ let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 let intros () =
-  apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
+  apply_tactic (PrimitiveTactics.intros_tac ~mknames:fresh_name)
 let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
 let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index 35122025cf2ef34bcaa6139ec0ef82154eac5c42..95b74ab99c7dde663a5a437cf5ce9da4f5fc1d5c 100644 (file)
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -189,7 +189,7 @@ let contradiction_tac ~status =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    T.then_ 
-      ~start: (P.intros_tac ~name:"FOO") 
+      ~start: (P.intros_tac ~mknames:(function () -> "FOO")) 
       ~continuation:(
         T.then_ 
            ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) 
@@ -495,7 +495,8 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
                                                        (* quale uguaglianza usare, eq o eqT ? *)
               ~continuations:[
                 T.then_ 
-                   ~start:(P.intros_tac ~name:"dummy_for_replace")
+                   ~start:
+                     (P.intros_tac ~mknames:(function () ->"dummy_for_replace"))
                    ~continuation:(T.then_ 
                                      ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
                                      ~continuation:(ProofEngineStructuralRules.clear