From c0f06261e5626228e4681de9973b6412524f09a2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 23 Jun 2005 12:30:26 +0000 Subject: [PATCH] Tactic discriminate activated in matita. --- helm/matita/matitaEngine.ml | 8 ++++---- helm/matita/tests/inversion.ma | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) 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 -- 2.39.2