diff options
| author | herbelin | 2007-10-03 12:31:45 +0000 |
|---|---|---|
| committer | herbelin | 2007-10-03 12:31:45 +0000 |
| commit | 1bead2a1ef23f2a281613093d7861815279e336d (patch) | |
| tree | 9eaf1b967dbd270e8525094ae3bed20e1cf260ee /parsing/pptactic.ml | |
| parent | 056af27f37f8fb9a00548c88047a86061a624e8b (diff) | |
Ajout de eelim, ecase, edestruct et einduction (expérimental).
Ajout de l'option with à (e)destruct et (e)induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c6c168d4ed..0190635273 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -427,8 +427,8 @@ let pr_clause_pattern pr_id = function let pr_orient b = if b then mt () else str " <-" -let pr_induction_arg prc = function - | ElimOnConstr c -> prc c +let pr_induction_arg prlc prc = function + | ElimOnConstr c -> pr_with_bindings prlc prc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) | ElimOnAnonHyp n -> int n @@ -680,11 +680,12 @@ and pr_atom1 = function | TacApply (ev,cb) -> hov 1 (str (if ev then "eapply" else "apply") ++ spc () ++ pr_with_bindings cb) - | TacElim (cb,cbo) -> - hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ + | TacElim (ev,cb,cbo) -> + hov 1 (str (if ev then "eelim" else "elim") ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c) - | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings cb) + | TacCase (ev,cb) -> + hov 1 (str (if ev then "ecase" else "case") ++ spc () ++ pr_with_bindings cb) | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c) | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> @@ -726,16 +727,16 @@ and pr_atom1 = function (* Derived basic tactics *) | TacSimpleInduction h -> hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) - | TacNewInduction (h,e,ids) -> - hov 1 (str "induction" ++ spc () ++ - prlist_with_sep spc (pr_induction_arg pr_constr) h ++ + | TacNewInduction (ev,h,e,ids) -> + hov 1 (str (if ev then "einduction" else "induction") ++ spc () ++ + prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ pr_with_names ids ++ pr_opt pr_eliminator e) | TacSimpleDestruct h -> hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) - | TacNewDestruct (h,e,ids) -> - hov 1 (str "destruct" ++ spc () ++ - prlist_with_sep spc (pr_induction_arg pr_constr) h ++ + | TacNewDestruct (ev,h,e,ids) -> + hov 1 (str (if ev then "edestruct" else "destruct") ++ spc () ++ + prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ pr_with_names ids ++ pr_opt pr_eliminator e) | TacDoubleInduction (h1,h2) -> |