Initial revision

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 69e8062eeddd17f10c667c7634c60f26c31b78bb..5f0ba8aaa97ee00f7c085f70386e17b5244e3484 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -224,7 +224,8 @@ let fold term =
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace =
     ProofEngineReduction.replace
-     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~equality:
+      (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
      ~what:term' ~with_what:term
    in
     let ty' = replace ty in
@@ -246,53 +247,6 @@ let fold term =
       proof := Some (curi,metasenv',pbo,pty) ;
       goal := Some metano
 
-exception NotConvertible
-
-(*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
-(*CSC: while [goal_input] can have a richer context (because of binders) *)
-(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
-(*CSC: Is that evident? Is that right? Or should it be changed?          *)
-let change ~goal_input ~input =
- let curi,metasenv,pbo,pty =
-  match !proof with
-     None -> assert false
-   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
-  match !goal with
-     None -> assert false
-   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
-  (* are_convertible works only on well-typed terms *)
-  ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
-  if CicReduction.are_convertible context goal_input input then
-   begin
-    let replace =
-     ProofEngineReduction.replace
-      ~equality:(==) ~what:goal_input ~with_what:input
-    in
-    let ty' = replace ty in
-    let context' =
-     List.map
-      (function
-          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
-        | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
-        | None -> None
-      ) context
-    in
-     let metasenv' = 
-      List.map
-       (function
-           (n,_,_) when n = metano -> (metano,context',ty')
-         | _ as t -> t
-       ) metasenv
-     in
-      proof := Some (curi,metasenv',pbo,pty) ;
-      goal := Some metano
-   end
-  else
-   raise NotConvertible
-
 (************************************************************)
 (*              Tactics defined elsewhere                   *)
 (************************************************************)
@@ -307,6 +261,8 @@ let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
 let elim_intros_simpl term =
   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
+let change ~goal_input:what ~input:with_what =
+  apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)
 
   (* structural tactics *)
 
@@ -318,4 +274,4 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
 let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
 let ring () = apply_tactic Ring.ring_tac
 let fourier () = apply_tactic FourierR.fourier_tac
-
+let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term)