diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 5 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/term.ml | 6 | ||||
| -rw-r--r-- | kernel/term.mli | 10 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | kernel/typeops.mli | 4 |
7 files changed, 22 insertions, 14 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 316e0735a9..e04a41f42b 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -224,6 +224,11 @@ module Spset = Set.Make(SpOrdered) module Spmap = Map.Make(SpOrdered) +(* Special references for inductive objects *) + +type inductive_path = section_path * int +type constructor_path = inductive_path * int + (* Hash-consing of name objects *) module Hident = Hashcons.Make( struct diff --git a/kernel/names.mli b/kernel/names.mli index 541e4f61a6..b3f5811e4c 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -70,6 +70,9 @@ val sp_gt : section_path * section_path -> bool module Spset : Set.S with type elt = section_path module Spmap : Map.S with type key = section_path +type inductive_path = section_path * int +type constructor_path = inductive_path * int + (* Hash-consing *) val hcons_names : unit -> (section_path -> section_path) * (section_path -> section_path) * diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 04d63da8ff..8f1ad37874 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -89,10 +89,10 @@ let rec execute mf env cstr = (make_judge cofix larv.(i), cst) | IsSort (Prop c) -> - (make_judge_of_prop_contents c, cst0) + (judge_of_prop_contents c, cst0) | IsSort (Type u) -> - make_judge_of_type u + judge_of_type u | IsAppL (f,args) -> let (j,cst1) = execute mf env f in diff --git a/kernel/term.ml b/kernel/term.ml index 1a5c74e682..38dbc37655 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -20,8 +20,8 @@ type 'a oper = (* DOPN *) | AppL | Const of section_path | Abst of section_path | Evar of int - | MutInd of section_path * int - | MutConstruct of (section_path * int) * int + | MutInd of inductive_path + | MutConstruct of constructor_path | MutCase of case_info | Fix of int array * int | CoFix of int @@ -30,7 +30,7 @@ type 'a oper = (* an extra slot, for putting in whatever sort of operator we need for whatever sort of application *) -and case_info = (section_path * int) option +and case_info = inductive_path option (* Sorts. *) diff --git a/kernel/term.mli b/kernel/term.mli index b849258606..6e7101ad34 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -17,14 +17,14 @@ type 'a oper = | Cast | Prod | Lambda | AppL | Const of section_path | Abst of section_path | Evar of int - | MutInd of section_path * int - | MutConstruct of (section_path * int) * int + | MutInd of inductive_path + | MutConstruct of constructor_path | MutCase of case_info | Fix of int array * int | CoFix of int | XTRA of string -and case_info = (section_path * int) option +and case_info = inductive_path option (*s The sorts of CCI. *) @@ -287,13 +287,13 @@ val args_of_abst : constr -> constr array (* Destructs a (co)inductive type *) val destMutInd : constr -> section_path * int * constr array -val op_of_mind : constr -> section_path * int +val op_of_mind : constr -> inductive_path val args_of_mind : constr -> constr array val ci_of_mind : constr -> case_info (* Destructs a constructor *) val destMutConstruct : constr -> section_path * int * int * constr array -val op_of_mconstr : constr -> (section_path * int) * int +val op_of_mconstr : constr -> constructor_path val args_of_mconstr : constr -> constr array (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0824c192cf..7066462452 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -357,13 +357,13 @@ let judge_of_set = uj_type = DOP0(Sort type_0); uj_kind = DOP0(Sort type_1) } -let make_judge_of_prop_contents = function +let judge_of_prop_contents = function | Null -> judge_of_prop | Pos -> judge_of_set (* Type of Type(i). *) -let make_judge_of_type u = +let judge_of_type u = let (uu,uuu,c) = super_super u in { uj_val = DOP0 (Sort (Type u)); uj_type = DOP0 (Sort (Type uu)); diff --git a/kernel/typeops.mli b/kernel/typeops.mli index b935efd8c6..a271dc9ecb 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -42,9 +42,9 @@ val type_case_branches : env -> 'a evar_map -> constr -> constr -> constr -> constr -> constr * constr array * constr -val make_judge_of_prop_contents : contents -> unsafe_judgment +val judge_of_prop_contents : contents -> unsafe_judgment -val make_judge_of_type : universe -> unsafe_judgment * constraints +val judge_of_type : universe -> unsafe_judgment * constraints val abs_rel : env -> 'a evar_map -> name -> typed_type -> unsafe_judgment |