1. change_tac moved from PrimitiveTactics to ReductionTactics

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 2f1d7be47de43c0ef3d36e8b5bd5a7a372b56761..3fefc662a5bcb7915e83ffb70bb9df4ea44a3bfd 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -586,55 +586,6 @@ let elim_intros_simpl_tac ~term =
    (Tacticals.thens
      ~start:(intros_tac ())
      ~continuations:
-       [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
+       [ReductionTactics.simpl_tac
+         ~pattern:(ProofEngineTypes.conclusion_pattern None)])
 ;;
-
-exception NotConvertible
-
-(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal,  *)
-(*CSC: while [what] can have a richer context (because of binders)           *)
-(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
-(*CSC: Is that evident? Is that right? Or should it be changed?              *)
-let change_tac ~what ~with_what =
-  let change_tac ~what ~with_what (proof, goal) =
-    let curi,metasenv,pbo,pty = proof in
-    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-      (* are_convertible works only on well-typed terms *)
-    let _,u = 
-      CicTypeChecker.type_of_aux' metasenv context with_what 
-       CicUniv.empty_ugraph
-    in (* TASSI: FIXME *)
-    let b,_ = 
-      CicReduction.are_convertible context what with_what u 
-    in
-      if b then
-       begin
-         let replace =
-           ProofEngineReduction.replace
-             ~equality:(==) ~what:[what] ~with_what:[with_what]
-         in
-         let ty' = replace ty in
-         let context' =
-           List.map
-             (function
-                  Some (name,Cic.Def (t,None))->
-                    Some (name,Cic.Def ((replace t),None))
-                | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
-                | None -> None
-                | Some (_,Cic.Def (_,Some _)) -> assert false
-             ) context
-         in
-         let metasenv' = 
-           List.map
-              (function
-                  (n,_,_) when n = metano -> (metano,context',ty')
-                | _ as t -> t
-              ) metasenv
-         in
-           (curi,metasenv',pbo,pty), [metano]
-       end
-      else
-       raise (ProofEngineTypes.Fail "Not convertible")
-  in
-    mk_tactic (change_tac ~what ~with_what)
-