diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-13 10:44:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-13 11:20:28 +0200 |
| commit | 24d0027f0344bca7abce3b8fa8c2a1e42ecf1a00 (patch) | |
| tree | bdde5a56a8e3ca5b0a258ccb68a85caf498fdf56 /toplevel | |
| parent | 9a4e062c92ad88c894ebbd6e20ee9d1511f24a3f (diff) | |
Providing a -type-in-type option for collapsing the universe hierarchy.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
3 files changed, 10 insertions, 4 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 74122d104..95cfd73a0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -434,7 +434,7 @@ let inductive_levels env evdref poly arities inds = (** Indices contribute. *) if Indtypes.is_indices_matter () && List.length ctx > 0 then ( let ilev = sign_level env !evdref ctx in - Evd.set_leq_sort evd (Type ilev) du) + Evd.set_leq_sort env evd (Type ilev) du) else evd in (** Constructors contribute. *) @@ -444,14 +444,14 @@ let inductive_levels env evdref poly arities inds = raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) else evd else - Evd.set_leq_sort evd (Type cu) du + Evd.set_leq_sort env evd (Type cu) du in let evd = if len >= 2 && Univ.is_type0m_univ cu then (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort evd (Prop Pos) du + Evd.set_leq_sort env evd (Prop Pos) du else evd in evd) !evdref (Array.to_list levels') destarities sizes diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c310986c6..3eee9658e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -70,6 +70,10 @@ let set_engagement c = engagement := Some c let engage () = match !engagement with Some c -> Global.set_engagement c | None -> () +let type_in_type = ref false +let set_type_in_type () = type_in_type := true +let set_hierarchy () = if !type_in_type then Global.set_type_in_type () + let set_batch_mode () = batch_mode := true let toplevel_default_name = DirPath.make [Id.of_string "Top"] @@ -430,6 +434,7 @@ let parse_args arglist = |"-quiet"|"-silent" -> Flags.make_silent true |"-quick" -> Flags.compilation_mode := BuildVi |"-time" -> Flags.time := true + |"-type-in-type" -> set_type_in_type () |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) |"-verbose-compat-notations" -> verb_compat_ntn := true @@ -494,6 +499,7 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); + set_hierarchy (); (* Be careful to set these variables after the inputstate *) Syntax_def.set_verbose_compat_notations !verb_compat_ntn; Syntax_def.set_compat_notations (not !no_compat_ntn); diff --git a/toplevel/record.ml b/toplevel/record.ml index ebaa6a911..d23338930 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -126,7 +126,7 @@ let typecheck_params_and_fields def id t ps nots fs = if Sorts.is_prop aritysort || (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then evars - else Evd.set_leq_sort evars (Type univ) aritysort + else Evd.set_leq_sort env_ar evars (Type univ) aritysort in let evars, nf = Evarutil.nf_evars_and_universes evars in let newps = map_rel_context nf newps in |