module Classops; ajout de fonctions dans Declare en consequence

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 17 insertions, 1 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 52355a7e28..909895612e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -135,6 +135,14 @@ let declare_mind mie =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
+(* Test and access functions. *)
+
+let is_constant sp = failwith "TODO"
+let constant_strength sp = failwith "TODO"
+
+let is_variable id = failwith "TODO"
+let variable_strength id = failwith "TODO"
+
 (* Global references. *)
 
 let first f v =
diff --git a/library/declare.mli b/library/declare.mli
index 9b0f969820..1b3b842cfb 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -31,6 +31,14 @@ val declare_mind : mutual_inductive_entry -> unit
 val declare_eliminations : section_path -> unit
 
 
+(*s Corresponding test and access functions. *)
+
+val is_constant : section_path -> bool
+val constant_strength : section_path -> strength
+
+val is_variable : identifier -> bool
+val variable_strength : identifier -> strength
+
 (*s It also provides a function [global_reference] to construct a global
   constr (a constant, an inductive or a constructor) from an identifier.
   To do so, it first looks for the section path using [Nametab.sp_of_id] and
diff --git a/library/redinfo.ml b/library/redinfo.ml
index 4e6c202156..dd1f32bd13 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -74,7 +74,7 @@ let constant_eval sp =
     v
   end
 
-(* Registration as global tables and roolback. *)
+(* Registration as global tables and rollback. *)
 
 type frozen = constant_evaluation Spmap.t