From 22b169aae0a2731e04dfa296d86bb8bbcbe12c9f Mon Sep 17 00:00:00 2001
From: bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 23 Jan 2003 20:29:57 +0000
Subject: Make sure proof by pointing works.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3605 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/centaur.ml4 | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'contrib/interface/centaur.ml4')

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index fe25cb07d..f51570394 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -330,13 +330,11 @@ let globcv x =
 	       (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
-(* <\cpa> 
 let pbp_tac_pcoq =
     pbp_tac (function (x:raw_tactic_expr) -> 
       output_results
         (ctf_header "pbp_results" !global_request_id)
        (Some (P_t(xlate_tactic x))));;
-</cpa> *)
 
 let blast_tac_pcoq =
     blast_tac (function (x:raw_tactic_expr) -> 
@@ -885,11 +883,12 @@ let command_creations = [
 ];;
 *)
 
-(* <\cpa> 
 TACTIC EXTEND Pbp
 | [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> 
     [ if_pcoq pbp_tac_pcoq idopt nl ]
 END
+
+(* <\cpa> 
 TACTIC EXTEND Blast
 | [ "Blast" ne_natural_list(nl) ] ->
     [ if_pcoq blast_tac_pcoq nl ]
-- 
cgit v1.2.3