From c330f60f1617afcb42cebe2fd2ccf9f330ea4f89 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 25 Jul 2000 17:29:20 +0000
Subject: retablissement make doc et make minicoq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacentries.mli | 2 +-
 tactics/tacticals.mli  | 8 +++++---
 2 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 6efd48d555..b364706ca1 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -15,7 +15,7 @@ val v_symmetry      : tactic_arg list -> tactic
 val v_transitivity  : tactic_arg list -> tactic
 val v_intro         : tactic_arg list -> tactic
 val v_introsUntil   : tactic_arg list -> tactic
-(*val v_tclIDTAC      : tactic_arg list -> tactic*)
+(*i val v_tclIDTAC      : tactic_arg list -> tactic i*)
 val v_assumption    : tactic_arg list -> tactic
 val v_exact         : tactic_arg list -> tactic
 val v_reduce        : tactic_arg list -> tactic
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 0cdedd8c68..4b89938276 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -37,8 +37,10 @@ val tclLAST_HYP      : (constr -> tactic) -> tactic
 val tclTRY_sign      : (constr -> tactic) -> var_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
-(*val dyn_tclIDTAC     : tactic_arg list -> tactic
-val dyn_tclFAIL      : tactic_arg list -> tactic*)
+(*i
+val dyn_tclIDTAC     : tactic_arg list -> tactic
+val dyn_tclFAIL      : tactic_arg list -> tactic
+i*)
 
 (*s Clause tacticals. *)
 
@@ -103,7 +105,7 @@ type branch_assumptions = {
   indargs   : identifier list} (* the inductive arguments *)
 
 val sort_of_goal      : goal sigma -> sorts
-(*val suff              : goal sigma -> constr -> string*)
+(*i val suff              : goal sigma -> constr -> string i*)
 
 val general_elim_then_using :
   constr ->  (inductive -> int -> bool list) -> 
-- 
cgit v1.2.3