From 476d70df227f6880e7fce29c30f2158f83ce05b9 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 19 Jul 2012 14:59:28 +0000
Subject: Getting rid of the undocumented [complete] tactic, which was
 redundant with [solve]. The AST node still exists in Ltac, because this is
 used by the [assert ... by ...] tactical. Fixes #2847.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15625 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f89877e004..6d921f85fe 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -916,7 +916,7 @@ let rec pr_tac inherited tac =
   | TacSolve tl ->
       str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
   | TacComplete t ->
-      str "complete" ++ spc () ++ pr_tac (lcomplete,E) t, lcomplete
+      pr_tac (lcomplete,E) t, lcomplete
   | TacId l ->
       str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
   | TacAtom (loc,TacAlias (_,s,l,_)) ->
-- 
cgit v1.2.3