diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 8 | ||||
| -rw-r--r-- | library/declare.mli | 8 | ||||
| -rw-r--r-- | library/redinfo.ml | 2 |
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 |