Improvement/bug fix: rewriting in the hypothesis used to simplify the

new hypothesis. This is no longer done.

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index b603bff9ed31b1cb48a6cbc54bae221ef0816333..7ed946170b5e36e018304c7062a033f96a4cb20c 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -54,7 +54,7 @@ let rec rewrite_tac ~direction ~pattern equality =
    | _ ->
   let arg,dir2,tac,concl_pat,gty =
    match hyps_pat with
-      [] -> None,true,PT.exact_tac,concl_pat,gty
+      [] -> None,true,(fun ~term _ -> PT.exact_tac term),concl_pat,gty
     | [name,pat] ->
       let rec find_hyp n =
        function
@@ -74,16 +74,17 @@ let rec rewrite_tac ~direction ~pattern equality =
        in
         let dummy = "dummy" in
         Some arg,false,
-         (fun ~term ->
+         (fun ~term typ ->
            Tacticals.seq
             ~tactics:
               [ProofEngineStructuralRules.rename name dummy;
                PT.letin_tac
                 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
                ProofEngineStructuralRules.clearbody name;
-               ReductionTactics.simpl_tac
+               ReductionTactics.change_tac
                 ~pattern:
-                  (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None);
+                  (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None)
+                (ProofEngineTypes.const_lazy_term typ);
                ProofEngineStructuralRules.clear dummy
               ]),
          pat,gty
@@ -153,23 +154,24 @@ let rec rewrite_tac ~direction ~pattern equality =
   let pred = C.Lambda (fresh_name, ty, abstr_gty) in
   (* The argument is either a meta if we are rewriting in the conclusion
      or the hypothesis if we are rewriting in an hypothesis *)
-  let metasenv',arg =
+  let metasenv',arg,newtyp =
    match arg with
       None ->
        let gty' = CicSubstitution.subst t2 abstr_gty in
        let irl =
         CicMkImplicit.identity_relocation_list_for_metavariable context in
        let metasenv' = (fresh_meta,context,gty')::metasenv' in
-        metasenv', C.Meta (fresh_meta,irl)
+        metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
     | Some arg ->
-       metasenv,arg
+       let gty' = CicSubstitution.subst t1 abstr_gty in
+        metasenv,arg,gty'
   in
   let exact_proof = 
     C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality]
   in
   let (proof',goals) =
     PET.apply_tactic 
-      (tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
+      (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal)
   in
   let goals =
    goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv