diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-28 09:24:15 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-28 09:24:15 +0000 |
| commit | f7665a72dba3a896997220d738597cfe05b27990 (patch) | |
| tree | 9bf47da71e2a912832199c6d13633d8ddee34678 /toplevel | |
| parent | 059a0622a512e40ffc1944cdc6084c3462aa85f9 (diff) | |
Fixes in generalize_eqs/dependent induction to allow the user to specify
generalized variables himself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a674bc3b7..ae9162860 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -825,7 +825,7 @@ let _ = let _ = declare_bool_option { optsync = true; - optname = "implicit arguments defensive printing"; + optname = "implicit status of reversible patterns"; optkey = (TertiaryTable ("Reversible","Pattern","Implicit")); optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } |