diff options
Diffstat (limited to 'printing/printer.ml')
-rw-r--r-- | printing/printer.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index e9d104b49..28b10c781 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -846,15 +846,6 @@ let pr_goal_by_uid uid = (* Elementary tactics *) let pr_prim_rule = function - | Cut (b,replace,id,t) -> - if b then - (* TODO: express "replace" *) - (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")") - else - let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in - (str"cut " ++ pr_constr t ++ - str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | Refine c -> (** FIXME *) str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ |