diff options
| -rw-r--r-- | kernel/entries.mli | 4 | ||||
| -rw-r--r-- | kernel/typeops.ml | 14 | ||||
| -rw-r--r-- | toplevel/command.ml | 5 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 5 | ||||
| -rw-r--r-- | toplevel/record.ml | 5 |
5 files changed, 17 insertions, 16 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index b2a77dd95..3ecfcca64 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -18,8 +18,8 @@ open Term (** {6 Local entries } *) type local_entry = - | LocalDef of constr - | LocalAssum of constr + | LocalDefEntry of constr + | LocalAssumEntry of constr (** {6 Declaration of inductive types. } *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index eeb12a2b4..0ea68e2bc 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -18,6 +18,7 @@ open Entries open Reduction open Inductive open Type_errors +open Context.Rel.Declaration let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y @@ -77,7 +78,6 @@ let judge_of_type u = (*s Type of a de Bruijn index. *) let judge_of_relative env n = - let open Context.Rel.Declaration in try let typ = get_type (lookup_rel n env) in { uj_val = mkRel n; @@ -99,9 +99,9 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = - let open Context.Named.Declaration in Context.Named.fold_outside (fun d1 () -> + let open Context.Named.Declaration in let id = get_id d1 in try let d2 = lookup_named id env in @@ -127,7 +127,6 @@ let extract_level env p = match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = - let open Context.Rel.Declaration in let fold l = function | LocalAssum (_,p) -> extract_level env p :: l | LocalDef _ -> l @@ -420,7 +419,6 @@ let type_fixpoint env lna lar vdefj = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = - let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -553,12 +551,12 @@ let infer_v env cv = (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDef c -> + | LocalDefEntry c -> let j = infer env c in - Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssum c -> + LocalDef (Name id, j.uj_val, j.uj_type) + | LocalAssumEntry c -> let j = infer env c in - Context.Rel.Declaration.LocalAssum (Name id, assumption_of_judgment env j) + LocalAssum (Name id, assumption_of_judgment env j) let infer_local_decls env decls = let rec inferec env = function diff --git a/toplevel/command.ml b/toplevel/command.ml index 166fe94ea..284bcd75e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -38,6 +38,7 @@ open Misctypes open Vernacexpr open Sigma.Notations open Context.Rel.Declaration +open Entries let do_universe poly l = Declare.do_universe poly l let do_constraint poly l = Declare.do_constraint poly l @@ -385,8 +386,8 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | LocalAssum (na,t) -> out_name na, Entries.LocalAssum t - | LocalDef (na,b,_) -> out_name na, Entries.LocalDef b + | LocalAssum (na,t) -> out_name na, LocalAssumEntry t + | LocalDef (na,b,_) -> out_name na, LocalDefEntry b (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 5fa51e06e..ffa11679c 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -14,6 +14,7 @@ open Vars open Entries open Declarations open Cooking +open Entries open Context.Rel.Declaration (********************************) @@ -21,8 +22,8 @@ open Context.Rel.Declaration let detype_param = function - | LocalAssum (Name id, p) -> id, Entries.LocalAssum p - | LocalDef (Name id, p,_) -> id, Entries.LocalDef p + | LocalAssum (Name id, p) -> id, LocalAssumEntry p + | LocalDef (Name id, p,_) -> id, LocalDefEntry p | _ -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace diff --git a/toplevel/record.ml b/toplevel/record.ml index 4cf81a250..c0bb9eb86 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -26,6 +26,7 @@ open Constrexpr_ops open Goptions open Sigma.Notations open Context.Rel.Declaration +open Entries (********** definition d'un record (structure) **************) @@ -164,8 +165,8 @@ let degenerate_decl decl = | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match decl with - | LocalAssum (_,t) -> (id, Entries.LocalAssum t) - | LocalDef (_,b,_) -> (id, Entries.LocalDef b) + | LocalAssum (_,t) -> (id, LocalAssumEntry t) + | LocalDef (_,b,_) -> (id, LocalDefEntry b) type record_error = | MissingProj of Id.t * Id.t list |