From 9e1372f77218ca6f0baf4ed7c590c91ad84b6313 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 25 Jun 2017 16:24:30 +0200
Subject: Moving "assert" (internally "Cut") to the new proof engine.

It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".
---
 printing/printer.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 3b0b6d5d2..6c571f424 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -845,15 +845,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 ") ++
-- 
cgit v1.2.3