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
---
 library/global.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index c2e8ac386c..b51ce3c774 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -25,11 +25,11 @@ val var_context : unit -> var_context
 
 val push_var_decl : identifier * constr -> unit
 val push_var_def : identifier * constr -> unit
-(*
+(*i
 val push_var : identifier * constr option * constr -> unit
 val push_rel_decl : name * constr -> unit
 val push_rel_def : name * constr -> unit
-*)
+i*)
 val add_constant : section_path -> constant_entry -> unit
 val add_parameter : section_path -> constr -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
@@ -38,7 +38,7 @@ val add_constraints : constraints -> unit
 val pop_vars : identifier list -> unit
 
 val lookup_var : identifier -> constr option * typed_type
-(*val lookup_rel : int -> name * typed_type*)
+(*i val lookup_rel : int -> name * typed_type i*)
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : inductive -> inductive_instance
-- 
cgit v1.2.3