diff options
| author | Pierre-Marie Pédrot | 2014-05-16 17:01:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-16 17:14:55 +0200 |
| commit | e321cfd21e28161923b84d943cb15c6d775b0d9e (patch) | |
| tree | f9acbdf0bf8c7ba8cf12b7282c6af700d8d7408f /printing/pptactic.ml | |
| parent | c2f78ed4fba9fa027fdf2051f214e1c5b4fe670e (diff) | |
Moving argument-free tactics out of the AST into a dedicated
"coretactics.ml4" file.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index ffb0d7a369..c7644f8c60 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -623,12 +623,10 @@ let pr_cofix_tac (id,c) = let rec pr_atom0 = function | TacIntroPattern [] -> str "intros" | TacIntroMove (None,MoveLast) -> str "intro" - | TacAssumption -> str "assumption" | 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") - | TacReflexivity -> str "reflexivity" | TacClear (true,[]) -> str "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" @@ -651,7 +649,6 @@ and pr_atom1 = function | TacIntroMove (ido,hto) -> hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscprint.pr_move_location pr_ident hto) - | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) @@ -799,7 +796,6 @@ and pr_atom1 = function pr_constr c ++ pr_clauses (Some true) pr_ident h) (* Equivalence relations *) - | TacReflexivity as x -> pr_atom0 x | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr_ident cls | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c | TacTransitivity None -> str "etransitivity" |