From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 proofs/logic.mli | 17 +++++------------
 1 file changed, 5 insertions(+), 12 deletions(-)

(limited to 'proofs/logic.mli')

diff --git a/proofs/logic.mli b/proofs/logic.mli
index da2566a7..420e6374 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -1,28 +1,24 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: logic.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Term
 open Sign
 open Evd
 open Environ
 open Proof_type
-(*i*)
 
-(* This suppresses check done in [prim_refiner] for the tactic given in
+(** This suppresses check done in [prim_refiner] for the tactic given in
    argument; works by side-effect *)
 
 val with_check    : tactic -> tactic
 
-(* [without_check] respectively means:\\
+(** [without_check] respectively means:\\
   [Intro]: no check that the name does not exist\\
   [Intro_after]: no check that the name does not exist and that variables in
      its type does not escape their scope\\
@@ -32,19 +28,16 @@ val with_check    : tactic -> tactic
   no check that the name exist and that its type is convertible\\
 *)
 
-(* The primitive refiner. *)
+(** The primitive refiner. *)
 
 val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
 
 type proof_variable
 
-val prim_extractor :
-  (proof_variable list -> proof_tree -> constr)
-  -> proof_variable list -> proof_tree -> constr
 
 val proof_variable_index : identifier -> proof_variable list -> int
 
-(*s Refiner errors. *)
+(** {6 Refiner errors. } *)
 
 type refiner_error =
 
-- 
cgit v1.2.3