- destruct tactic: automatic simplification in case of failure removed

[helm.git] / helm / software / components / tactics / reductionTactics.ml

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 5afc672695733cada18b7335705e1d360bec515b..9c39caa6f4cee2a4f03fbf505591398a65c24fda 100644 (file)
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -30,7 +30,7 @@ open ProofEngineTypes
 (* Note: this code is almost identical to change_tac and
 *  it could be unified by making the change function a callback *)
 let reduction_tac ~reduction ~pattern (proof,goal) =
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -88,7 +88,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
       | _ as t -> t
     ) metasenv
   in
-  (curi,metasenv',pbo,pty, attrs), [metano]
+  (curi,metasenv',_subst,pbo,pty, attrs), [metano]
 ;;
 
 let simpl_tac ~pattern =
@@ -119,11 +119,6 @@ let normalize_tac ~pattern =
   ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
 
 let head_beta_reduce_tac ?delta ?upto ~pattern =
- begin match upto with
-    | Some upto -> 
-         HLog.warn (Printf.sprintf "inside head_beta_reduce_tac %i" upto)
-    | None -> HLog.warn (Printf.sprintf "inside head_beta_reduce_tac none")
- end;
  mk_tactic (reduction_tac
   ~reduction:
     (const_lazy_reduction
@@ -140,9 +135,9 @@ exception NotConvertible
         reference variables that are local to the term that is going to be
         replaced. To fix this we should parse with_what in the context of the
         term(s) to be replaced. *)
-let change_tac ~pattern with_what  =
+let change_tac ?(with_cast=false) ~pattern with_what  =
  let change_tac ~pattern ~with_what (proof, goal) =
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -211,7 +206,19 @@ let change_tac ~pattern with_what  =
         | _ as t -> t)
       metasenv
   in
-  (curi,metasenv',pbo,pty, attrs), [metano]
+   let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in
+    if with_cast then
+     let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in
+     let (newproof,_) =
+       let irl= CicMkImplicit.identity_relocation_list_for_metavariable context'
+       in
+        ProofEngineHelpers.subst_meta_in_proof
+         proof metano
+          (Cic.Cast (Cic.Meta(metano',irl),ty')) [metano',context',ty']
+     in
+      newproof, [metano']
+    else
+     proof,[goal]
   in
     mk_tactic (change_tac ~pattern ~with_what)