diff options
| author | herbelin | 2002-10-21 13:07:30 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-21 13:07:30 +0000 |
| commit | 04ceaad7583afcd85754b909ae25e7128646ff54 (patch) | |
| tree | b45b773df0b73bf4e057b62c2b722e894a700745 /parsing/pptactic.ml | |
| parent | b6fead62658797f75be03d1a952b771f4c260c0f (diff) | |
NewDestruct/NewInduction acceptent l'option "using"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index a448166e1c..e0f8bd3f1e 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -303,6 +303,7 @@ let make_pr_tac (pr_constr,pr_cst,pr_ind,pr_ident,pr_extend) = let pr_bindings = pr_bindings pr_constr in let pr_with_bindings = pr_with_bindings pr_constr in +let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in let pr_constrarg c = spc () ++ pr_constr c in let pr_intarg n = spc () ++ int n in @@ -339,10 +340,9 @@ and pr_atom1 = function | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c) | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb) - | TacElim (cb,None) -> hov 1 (str "Elim" ++ spc () ++ pr_with_bindings cb) - | TacElim (cb,Some cb') -> + | TacElim (cb,cbo) -> hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++ - spc () ++ str "using" ++ pr_arg pr_with_bindings cb') + pr_opt pr_eliminator cbo) | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c) | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb) | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c) @@ -383,12 +383,14 @@ and pr_atom1 = function (* Derived basic tactics *) | TacOldInduction h -> hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h) - | TacNewInduction h -> - hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h) + | TacNewInduction (h,e) -> + hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++ + pr_opt pr_eliminator e) | TacOldDestruct h -> hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h) - | TacNewDestruct h -> - hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h) + | TacNewDestruct (h,e) -> + hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++ + pr_opt pr_eliminator e) | TacDoubleInduction (h1,h2) -> hov 1 (str "Double Induction" ++ |