diff options
| author | Pierre-Marie Pédrot | 2016-05-17 22:37:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 22:38:40 +0200 |
| commit | f7fb1918619fcef384d4aa84938246de67c707fa (patch) | |
| tree | 6f8b1b8ba71681b06b4a74ddeee76d02a3ef09dd /printing/printer.ml | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
| parent | dadd4003b6607ccc103658f842b5efbd6d8ab57f (diff) | |
Putting all the tactics exported by the Tactics module in the new monad API.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index a16a92d0a5..cb075c64fb 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -685,35 +685,10 @@ let pr_prim_rule = function (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | FixRule (f,n,[],_) -> - (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth - | [] -> mt () in - (str"fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[],_) -> - (str"cofix " ++ pr_id f) - - | Cofix (f,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) - | [] -> mt () in - (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) | Refine c -> str(if Termops.occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c - | Thin ids -> - (str"clear " ++ pr_sequence pr_id ids) - | Move (id1,id2) -> (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) |