From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 23 Jun 2005 12:30:26 +0000 (+0000)
Subject: Tactic discriminate activated in matita.
X-Git-Tag: INDEXING_NO_PROOFS~93
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0f06261e5626228e4681de9973b6412524f09a2;p=helm.git

Tactic discriminate activated in matita.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 7302e3bde..669d7b62f 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -30,9 +30,7 @@ let tactic_of_ast = function
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
-(*
-  | TacticAst.Discriminate (_,id) -> Tactics.discriminate id
-*)
+  | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
   | TacticAst.Exists _ -> Tactics.exists
   | TacticAst.Fourier _ -> Tactics.fourier
   | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat
@@ -414,12 +412,14 @@ let disambiguate_tactic status = function
       let status,term = disambiguate_term status term in
       let pattern = disambiguate_pattern status.aliases pattern in
       status, TacticAst.Generalize(loc,term,pattern)
+  | TacticAst.Discriminate (loc,term) ->
+      let status,term = disambiguate_term status term in
+      status, TacticAst.Discriminate(loc,term)
 (*
   (* TODO Zack a lot more of tactics to be implemented here ... *)
   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
   | TacticAst.Change of 'term * 'term * 'ident option
   | TacticAst.Decompose of 'ident * 'ident list
-  | TacticAst.Discriminate of 'ident
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
   | TacticAst.Replace_pattern of 'term pattern * 'term
diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
index ccbc4d96b..e61e123d7 100644
--- a/helm/matita/tests/inversion.ma
+++ b/helm/matita/tests/inversion.ma
@@ -18,5 +18,5 @@ theorem test_inversion: \forall n. le n O \to n=O.
   apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
   intro. reflexivity.
   simplify. intros.
-  (* manca discriminate H3 *)
+  discriminate H3.
 qed.
\ No newline at end of file