]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/primitiveTactics.ml
Typing of intros_tac improved. It now has a parameter that is a fresh-names
[helm.git] / helm / gTopLevel / primitiveTactics.ml
index 8b3f025aa07a575e9e9015528010d725b9bee5f7..eba2d571ff8d4fc26ed633f375f3be1fd89872cd 100644 (file)
@@ -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")))
 ;;