diff options
| author | glondu | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /kernel/pre_env.mli | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 518c6330d8..abbf9b1b53 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -18,10 +18,10 @@ open Declarations (* The type of environments. *) -type key = int option ref +type key = int option ref type constant_key = constant_body * key - + type globals = { env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; @@ -34,7 +34,7 @@ type stratification = { env_engagement : engagement option } -type val_kind = +type val_kind = | VKvalue of values * Idset.t | VKnone @@ -49,7 +49,7 @@ type env = { env_rel_context : rel_context; env_rel_val : lazy_val list; env_nb_rel : int; - env_stratification : stratification; + env_stratification : stratification; retroknowledge : Retroknowledge.retroknowledge } type named_context_val = named_context * named_vals @@ -63,14 +63,14 @@ val empty_env : env val nb_rel : env -> int val push_rel : rel_declaration -> env -> env val lookup_rel_val : int -> env -> lazy_val -val env_of_rel : int -> env -> env +val env_of_rel : int -> env -> env (* Named context *) -val push_named_context_val : +val push_named_context_val : named_declaration -> named_context_val -> named_context_val val push_named : named_declaration -> env -> env val lookup_named_val : identifier -> env -> lazy_val -val env_of_named : identifier -> env -> env +val env_of_named : identifier -> env -> env (* Global constants *) |