diff options
| author | Pierre-Marie Pédrot | 2016-10-12 21:14:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-12 21:14:07 +0200 |
| commit | 05ad4f49ac2203dd64dfec79a1fc62ee52115724 (patch) | |
| tree | 920faae7946821c093345fd1804c40336bd9f1c4 /interp | |
| parent | 8a6c792505160de4ba2123ef049ab45d28873e47 (diff) | |
| parent | 0222f685ebdd55a1596d6689b96ebb86454ba1a7 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f7fcbb4eed..4aff82403e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -481,7 +481,7 @@ let explicitize loc inctx impl (cf,f) args = (!print_implicits && !print_implicits_explicit_args) || (is_needed_for_correct_partial_application tail imp) || (!print_implicits_defensive && - (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) && + (not (is_inferable_implicit inctx n imp) || !Flags.beautify) && is_significant_implicit (Lazy.force a)) in if visible then diff --git a/interp/topconstr.ml b/interp/topconstr.ml index eb564f3b32..b455381ea3 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -22,8 +22,7 @@ open Constrexpr_ops let asymmetric_patterns = ref (false) let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; - Goptions.optname = - "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments"; + Goptions.optname = "no parameters in constructors"; Goptions.optkey = ["Asymmetric";"Patterns"]; Goptions.optread = (fun () -> !asymmetric_patterns); Goptions.optwrite = (fun a -> asymmetric_patterns:=a); |