Never implemented tactics compare and decide equality purged from the code.

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 6c51fc80abf190dc8898985ebfb50215097041f1..20635bd648accbf1e53f4d8717eebe0e2d61c9c8 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -53,11 +53,9 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Clear of loc * 'ident
   | ClearBody of loc * 'ident
-  | Compare of loc * 'term
   | Constructor of loc * int
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
-  | DecideEquality of loc
   | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
   | Discriminate of loc * 'term
   | Elim of loc * 'term * 'term option * int option * 'ident list

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 8bd5c96f15862677345877c9487e4ce6a96c5501..d6502aca80dae87f36db7c05f923e98c6eeb8042 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -78,13 +78,11 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,id) -> sprintf "clear %s" id
   | ClearBody (_,id) -> sprintf "clearbody %s" id
-  | Compare (_,term) -> "compare " ^ term_pp term
   | Constructor (_,n) -> "constructor " ^ string_of_int n
   | Contradiction _ -> "contradiction"
   | Cut (_, ident, term) ->
      "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
-  | DecideEquality _ -> "decide equality"
   | Decompose (_, [], what, names) ->
       sprintf "decompose %s%s" what (pp_intros_specs (None, names)) 
   | Decompose (_, types, what, names) ->

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 65dd17b6a096c1e144daf7068e80cf49cba2ce2d..c55bf8d9ebecb5296304548c296d6f42a0b17426 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -67,12 +67,10 @@ let tactic_of_ast ast =
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
-  | GrafiteAst.Compare (_, term) -> Tactics.compare term
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
   | GrafiteAst.Cut (_, ident, term) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
-  | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
   | GrafiteAst.Decompose (_, types, what, names) -> 
       let to_type = function
          | GrafiteAst.Type (uri, typeno) -> uri, typeno

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index f5ea66f2f6883e06a840744579277817577fe32f..26c74e657afe317600598f3fe4e84f8886cf155d 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -112,9 +112,6 @@ let disambiguate_tactic lexicon_status_ref context metasenv tactic =
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
-    | GrafiteAst.Compare (loc,term) ->
-        let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Compare (loc,term)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->
@@ -122,8 +119,6 @@ let disambiguate_tactic lexicon_status_ref context metasenv tactic =
     | GrafiteAst.Cut (loc, ident, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Cut (loc, ident, cic)
-    | GrafiteAst.DecideEquality loc ->
-        metasenv,GrafiteAst.DecideEquality loc
     | GrafiteAst.Decompose (loc, types, what, names) ->
         let disambiguate (metasenv,types) = function
            | GrafiteAst.Type _   -> assert false

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index e480efd34f1cbfbc77656716ee0f4f9ff0b59f66..73d6bf66ac5e3f8c37865cacbd7719fb092cf8eb 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -140,16 +140,12 @@ EXTEND
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
-    | IDENT "compare"; t = tactic_term ->
-        GrafiteAst.Compare (loc,t)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decide"; IDENT "equality" ->
-        GrafiteAst.DecideEquality loc
     | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
       (num, idents) = intros_spec ->
         let types = match types with None -> [] | Some types -> types in

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 9e5bc7f43e1d3885225d6f3ecd24dbab01faab73..0ffa2c52b4ceb70d0bff28a98a7182e4611c8b60 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -341,66 +341,6 @@ let discriminate_tac ~term =
  in
   ProofEngineTypes.mk_tactic (discriminate_tac ~term)
 
-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 = Tacticals.id_tac
- (*
-(* 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 = CicUtil.lookup_meta 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:term')
-               ~continuations:[
-                 T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
-                 decide_equality_tac]  
-               status
-      | (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:term')
-               ~continuations:[
-                 T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
-                 decide_equality_tac]  
-               status
-      | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") 
-*)
-;;
-
-
-
 (* DISCRIMINTATE SENZA INJECTION 
 
 exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int) 

diff --git a/helm/software/components/tactics/discriminationTactics.mli b/helm/software/components/tactics/discriminationTactics.mli
index f1153256f51e10c020a7bb19b6ce9b5c6fd79d7a..5815bb551a0d5c34e4a0b2c59f8339a2a53cd7a9 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.mli
+++ b/helm/software/components/tactics/discriminationTactics.mli
@@ -25,6 +25,3 @@
 
 val injection_tac: term:Cic.term -> ProofEngineTypes.tactic
 val discriminate_tac: term:Cic.term -> ProofEngineTypes.tactic
-val decide_equality_tac: ProofEngineTypes.tactic
-val compare_tac: term:Cic.term -> ProofEngineTypes.tactic
-

diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml
index fe8adc549f67ef388656d81c3e7fcdf71c6f3cf7..4d52725891e04f5e2e24ca2d4ec8ae367366fe40 100644 (file)
--- a/helm/software/components/tactics/tactics.ml
+++ b/helm/software/components/tactics/tactics.ml
@@ -32,11 +32,9 @@ let auto = AutoTactic.auto_tac
 let change = ReductionTactics.change_tac
 let clear = ProofEngineStructuralRules.clear
 let clearbody = ProofEngineStructuralRules.clearbody
-let compare = DiscriminationTactics.compare_tac
 let constructor = IntroductionTactics.constructor_tac
 let contradiction = NegationTactics.contradiction_tac
 let cut = PrimitiveTactics.cut_tac
-let decide_equality = DiscriminationTactics.decide_equality_tac
 let decompose = EliminationTactics.decompose_tac
 let demodulate = Saturation.demodulate_tac
 let discriminate = DiscriminationTactics.discriminate_tac

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index c8c225cddd2ae8a8015f8d3b241aecffa23c635b..211897a8a02506c76357869294f97338d9c1bb35 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -12,13 +12,11 @@ val change :
   Cic.lazy_term -> ProofEngineTypes.tactic
 val clear : hyp:string -> ProofEngineTypes.tactic
 val clearbody : hyp:string -> ProofEngineTypes.tactic
-val compare : term:Cic.term -> ProofEngineTypes.tactic
 val constructor : n:int -> ProofEngineTypes.tactic
 val contradiction : ProofEngineTypes.tactic
 val cut :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term -> ProofEngineTypes.tactic
-val decide_equality : ProofEngineTypes.tactic
 val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int) list ->

diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index d0223158856eeee49980978b26deaa3eee60357d..f53d833b6013965926927fde840608e3d8f45223 100644 (file)
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -87,11 +87,9 @@
     <keyword>clear</keyword>
     <keyword>clearbody</keyword>
     <keyword>change</keyword>
-    <keyword>compare</keyword>
     <keyword>constructor</keyword>
     <keyword>contradiction</keyword>
     <keyword>cut</keyword>
-    <keyword>decide</keyword> <keyword>equality</keyword> <!-- CSC: ??? -->
     <keyword>decompose</keyword>
     <keyword>discriminate</keyword>
     <keyword>elim</keyword>