Added module DiscriminationTactics with brand new tactics Injection and

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index f24f7904cab829e01a01ff1e0588c3c044d6a239..390d97fb774b306baa0ea183612ea75ea1c961f7 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -56,7 +56,10 @@ exception AllSelectedTermsMustBeConvertible;;
 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
-let generalize_tac ~terms ~status:((proof,goal) as status) =
+let generalize_tac
+ ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ terms ~status:((proof,goal) as status)
+=
   let module C = Cic in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
@@ -78,7 +81,7 @@ let generalize_tac ~terms ~status:((proof,goal) as status) =
       ~start:
         (P.cut_tac 
          (C.Prod(
-           (C.Name "dummy_for_gen"), 
+           (mk_fresh_name_callback context C.Anonymous typ), 
            typ,
            (ProofEngineReduction.replace_lifting_csc 1
              ~equality:(==) 
@@ -91,70 +94,3 @@ let generalize_tac ~terms ~status:((proof,goal) as status) =
 ;;
 
 
-(* IN FASE DI IMPLEMENTAZIONE *)
-
-let decide_equality_tac =
-(* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza
-e' vera o no e lo risolve *)
-  Tacticals.id_tac
-;;
-
-
-let compare_tac ~term ~status:((proof, goal) as status) =
-(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to          *)
-(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2  *)
-  let module C = Cic in
-  let module U = UriManager in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-    let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
-     let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
-      match termty with
-         (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
-          
-          let term' = (* (t1=t2)\/~(t1=t2) *)
-           C.Appl [
-            (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; 
-            term ; 
-            C.Appl [
-             (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ; 
-             t1 ; 
-             C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
-            ]
-           ] 
-          in
-            T.thens 
-               ~start:(P.cut_tac term')
-               ~continuations:[
-                 T.then_ ~start:(P.intros_tac ()) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
-                 decide_equality_tac]  
-      | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
-          let term' = (* (t1=t2) \/ ~(t1=t2) *)
-           C.Appl [
-            (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; 
-            term ; 
-            C.Appl [
-             (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ; 
-             t1 ; 
-             C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
-            ]
-           ] 
-          in
-            T.thens 
-               ~start:(P.cut_tac term')
-               ~continuations:[
-                 T.then_ ~start:(P.intros_tac ()) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
-                 decide_equality_tac]  
-      | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") 
-;;
-
-
-let discriminate_tac ~term ~status:((proof, goal) as status) =
-  let module C = Cic in
-  let module U = UriManager in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-   T.id_tac 
-;;
-