X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=91cd6198ef8bb28d6d60f7a42a8450fdfa62bcc8;hb=4c9da07604c4f8b66e4e92861ee38129422d23fb;hp=ccd8ccfe0ad63eddcd5c572092a78fd11d2ece72;hpb=261ccc2ead2f1816d1f0293f7505e04f7a68b5cd;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index ccd8ccfe0..91cd6198e 100644
--- 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 mknames =
+let lambda_abstract 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' = C.Name (mknames n) in
+       let n' = mk_fresh_name context n ~typ:s in
         let (context',ty,bo) =
          collect_context ((Some (n',(C.Decl s)))::context) t
         in
@@ -112,7 +112,10 @@ let eta_expand metasenv context t arg =
    let argty =
     T.type_of_aux' metasenv context arg
    in
-    (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
+    let fresh_name =
+     ProofEngineHelpers.mk_fresh_name context (Cic.Name "Heta") ~typ:argty
+    in
+     (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg])
 
 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
 let classify_metas newmeta in_subst_domain subst_in metasenv =
@@ -301,35 +304,43 @@ let apply_tac ~term ~status =
   with CicUnification.UnificationFailed as e ->
     raise (Fail (Printexc.to_string e))
 
-let intros_tac ~status:(proof, goal) =
+let intros_tac
+ ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name) ()
+ ~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 (ProofEngineHelpers.fresh_name)
+     lambda_abstract context newmeta ty mk_fresh_name_callback
     in
      let (newproof, _) =
        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
      in
       (newproof, [newmeta])
 
-let cut_tac ~term ~status:(proof, goal) =
+let cut_tac
+ ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ term ~status:(proof, goal)
+=
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let newmeta1 = new_meta ~proof in
    let newmeta2 = newmeta1 + 1 in
+   let fresh_name =
+    mk_fresh_name_callback context (Cic.Name "Hcut") ~typ:term in
    let context_for_newmeta1 =
-    (Some (C.Name "dummy_for_cut",C.Decl term))::context in
+    (Some (fresh_name,C.Decl term))::context in
    let irl1 =
     identity_relocation_list_for_metavariable context_for_newmeta1 in
    let irl2 = identity_relocation_list_for_metavariable context in
     let newmeta1ty = CicSubstitution.lift 1 ty in
     let bo' =
      C.Appl
-      [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ;
+      [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ;
        C.Meta (newmeta2,irl2)]
     in
      let (newproof, _) =
@@ -338,18 +349,23 @@ let cut_tac ~term ~status:(proof, goal) =
      in
       (newproof, [newmeta1 ; newmeta2])
 
-let letin_tac ~term ~status:(proof, goal) =
+let letin_tac
+ ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ term ~status:(proof, goal)
+=
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let _ = CicTypeChecker.type_of_aux' metasenv context term in
     let newmeta = new_meta ~proof in
+    let fresh_name =
+     mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in
     let context_for_newmeta =
-     (Some (C.Name "dummy_for_letin",C.Def term))::context in
+     (Some (fresh_name,C.Def term))::context in
     let irl =
      identity_relocation_list_for_metavariable context_for_newmeta in
      let newmetaty = CicSubstitution.lift 1 ty in
-     let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in
+     let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
       let (newproof, _) =
         subst_meta_in_proof
           proof metano bo'[newmeta,context_for_newmeta,newmetaty]
@@ -505,9 +521,9 @@ let elim_intros_simpl_tac ~term =
  Tacticals.then_ ~start:(elim_tac ~term)
   ~continuation:
    (Tacticals.thens
-     ~start:intros_tac
+     ~start:(intros_tac ())
      ~continuations:
-       [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None])
+       [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None])
 ;;
 
 exception NotConvertible
@@ -524,7 +540,8 @@ let change_tac ~what ~with_what ~status:(proof, goal) =
   if CicReduction.are_convertible context what with_what then
    begin
     let replace =
-     ProofEngineReduction.replace ~equality:(==) ~what ~with_what
+     ProofEngineReduction.replace
+      ~equality:(==) ~what:[what] ~with_what:[with_what]
     in
     let ty' = replace ty in
     let context' =