From d37aab528dca587127b9f9944e1521e4fc3d9cc7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 7 Oct 2015 13:11:52 +0200
Subject: Univs: add Strict Universe Declaration option (on by default)

This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
---
 printing/ppconstr.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 650b8f7262..ea705e335e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -140,8 +140,8 @@ end) = struct
 
   let pr_univ l =
     match l with
-      | [x] -> str x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+      | [_,x] -> str x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -174,7 +174,7 @@ end) = struct
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some u -> str u
+        | Some (_,u) -> str u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
-- 
cgit v1.2.3


From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Oct 2015 14:11:19 +0200
Subject: Goptions: new value type: optional string

These options can be set to a string value, but also unset.
Internal data is of type string option.
---
 printing/ppvernac.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 71dcd15cc7..76f97fce1e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -166,6 +166,8 @@ module Make
     (* This should not happen because of the grammar *)
       | IntValue (Some n) -> spc() ++ int n
       | StringValue s -> spc() ++ str s
+      | StringOptValue None -> mt()
+      | StringOptValue (Some s) -> spc() ++ str s
       | BoolValue b -> mt()
     in pr_printoption a None ++ pr_opt_value b
 
-- 
cgit v1.2.3


From 33d153a01f2814c6e5486c07257667254b91fa0c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Oct 2015 15:08:27 +0200
Subject: Axioms now support the universe binding syntax.

We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
---
 printing/ppvernac.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 76f97fce1e..00c276bdbe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -356,6 +356,7 @@ module Make
       | l ->
         prlist_with_sep spc
           (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+
 (*
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
@@ -774,11 +775,12 @@ module Make
           return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
         | VernacAssumption (stre,_,l) ->
           let n = List.length (List.flatten (List.map fst (List.map snd l))) in
-          return (
-            hov 2
-              (pr_assumption_token (n > 1) stre ++ spc() ++
-                 pr_ne_params_list pr_lconstr_expr l)
-          )
+          let pr_params (c, (xl, t)) =
+            hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++
+              (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t))
+          in
+          let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
+          return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions))
         | VernacInductive (p,f,l) ->
           let pr_constructor (coe,(id,c)) =
             hov 2 (pr_lident id ++ str" " ++
-- 
cgit v1.2.3