diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 5 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
2 files changed, 0 insertions, 6 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 7d919956e8..506a8dc5b0 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -32,10 +32,6 @@ 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] @@ -526,7 +522,6 @@ 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 051638d53c..6848862603 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -81,7 +81,6 @@ 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)\ |