From d7b2414b631d71e89e677d650b84bd4fadd44895 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Jan 2005 17:18:23 +0000
Subject: Compatibilité ocamlweb pour cible doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.mli | 2 +-
 proofs/refiner.mli      | 1 -
 proofs/tacmach.mli      | 3 ---
 3 files changed, 1 insertion(+), 5 deletions(-)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 57312cb4b7..090671e046 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -23,4 +23,4 @@ val w_refine :  env -> evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
 val instantiate_pf_com :
   int -> Topconstr.constr_expr -> pftreestate -> pftreestate
 
-(* the instantiate tactic was moved to tactics/evar_tactics.ml *) 
+(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3a0faa7221..b21485e456 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,4 +1,3 @@
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 22b9de0b73..66cb97fac8 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -119,9 +119,6 @@ val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   evar_map -> pftreestate -> pftreestate
 
-(*
-val vernac_tactic : string * tactic_arg list -> tactic
-*)
 (*s The most primitive tactics. *)
 
 val refiner                   : rule -> tactic
-- 
cgit v1.2.3