attributes stripped from searchPattern query (as in the new query generator)

[helm.git] / helm / ocaml / tactics / equalityTactics.ml

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 29df82c08ab5f21f121a688231ecf98d46058836..8cb794ff6e17e918eefd4f0696276a41fc806822 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -56,11 +56,11 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
-      C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+      C.Lambda
+       (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
     let fresh_meta = ProofEngineHelpers.new_meta proof in
     let irl =
      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
@@ -81,7 +81,7 @@ let rewrite_simpl_tac ~term ~status =
  Tacticals.then_ 
   ~start:(rewrite_tac ~term)
   ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
   ~status
 ;;
 
@@ -118,11 +118,11 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
-      C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+      C.Lambda
+       (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
     let fresh_meta = ProofEngineHelpers.new_meta proof in
     let irl =
      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
@@ -144,7 +144,7 @@ let rewrite_back_simpl_tac ~term ~status =
  Tacticals.then_ 
   ~start:(rewrite_back_tac ~term)
   ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
   ~status
 ;;
 
@@ -169,11 +169,10 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
                      with_what]))
               ~continuations:[
                 T.then_
-                   ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
+                   ~start:(rewrite_back_tac ~term:(C.Rel 1))
                    ~continuation:(
                      ProofEngineStructuralRules.clear
                       ~hyp:(List.hd context)) ;
-(*                                                     (Some(C.Name "dummy_for_replace" , C.Def (CicTypeChecker.type_of_aux' metasenv context (C.Rel 1)) (* NOOOO!!!!! tipo di dummy *) )))) ; *)
                 T.id_tac]
               ~status
        else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")