diff options
| author | Pierre-Marie Pédrot | 2014-08-07 00:19:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-07 01:12:59 +0200 |
| commit | 07a9afbdf9561402897728963d40de80b9912bea (patch) | |
| tree | e30c0599ecccad324425d2c1ace2cde846cf5bf3 /printing/pptactic.ml | |
| parent | fe3b935204b8e4889b969bfd2faaaaa679e8a3cf (diff) | |
Removing the "constructor" tactic from the AST.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 1535bab9a7..24f374b179 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -646,8 +646,6 @@ let pr_cofix_tac (id,c) = let rec pr_atom0 = function | TacIntroPattern [] -> str "intros" | TacIntroMove (None,MoveLast) -> str "intro" - | TacAnyConstructor (false,None) -> str "constructor" - | TacAnyConstructor (true,None) -> str "econstructor" | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial") | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto") | TacClear (true,[]) -> str "clear" @@ -780,9 +778,6 @@ and pr_atom1 = function (* Constructors *) | TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l) - | TacAnyConstructor (ev,Some t) -> - hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t) - | TacAnyConstructor (ev,None) as t -> pr_atom0 t | TacConstructor (ev,n,l) -> hov 1 (str (with_evars ev "constructor") ++ pr_or_var pr_intarg n ++ pr_bindings l) |