From 96ed527472c38e92727d8fb6bfc41770c43b762b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Oct 2016 22:11:16 +0200
Subject: Fixing a few confusions on the name of the beautify flag. (It should
 apply also interactively.)

---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e71daef999..afc1c4caf8 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
-- 
cgit v1.2.3


From 5539201bf25dec1b5c24634dca581e199caca4e7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Oct 2016 12:02:21 +0200
Subject: Shorter message for "Test Asymmetric Patterns".

But maybe it is that how the "Test" message is elaborated is not
intuitive...
---
 interp/topconstr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2b860173a6..79eeacf354 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);
-- 
cgit v1.2.3