diff options
| author | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
| commit | 083e83a2e82c17c13b5af7d59029d4ef0aa1b613 (patch) | |
| tree | 7609e9b92c93fe21603aaa2f7d90805e30812f53 /toplevel | |
| parent | 1f74267d7e4affe14dbafc1a6f1e6f3f465f75a8 (diff) | |
| parent | 24a9a9c4bef18133c0b5070992d3396ff7596a7c (diff) | |
Merge PR #9918: Fix #9294: critical bug with template polymorphism
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 5 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
2 files changed, 6 insertions, 0 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 64c1da20b6..0490c35970 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -32,6 +32,10 @@ let set_type_in_type () = let typing_flags = Environ.typing_flags (Global.env ()) in Global.set_typing_flags { typing_flags with Declarations.check_universes = false } +let set_no_template_check () = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_template = false } + (******************************************************************************) type color = [`ON | `AUTO | `EMACS | `OFF] @@ -525,6 +529,7 @@ let parse_args ~help ~init arglist : t * string list = |"-list-tags" -> set_query oval PrintTags |"-time" -> { oval with config = { oval.config with time = true }} |"-type-in-type" -> set_type_in_type (); oval + |"-no-template-check" -> set_no_template_check (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index cdb2e36fbd..8555d78156 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -82,6 +82,7 @@ let print_usage_common co command = \n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -no-template-check disable checking of universes constraints on universes parameterizing template polymorphic inductive types\ \n -mangle-names x mangle auto-generated names using prefix x\ \n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ \n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ |