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.
---
 intf/misctypes.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 74e136904d..5c11119ed8 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -44,8 +44,8 @@ type 'id move_location =
 (** Sorts *)
 
 type 'a glob_sort_gen = GProp | GSet | GType of 'a
-type sort_info = string list
-type level_info = string option
+type sort_info = string Loc.located list
+type level_info = string Loc.located option
 
 type glob_sort = sort_info glob_sort_gen
 type glob_level = level_info glob_sort_gen
-- 
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.
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 37218fbf91..9248fa953c 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -155,6 +155,7 @@ type option_value = Goptions.option_value =
   | BoolValue of bool
   | IntValue of int option
   | StringValue of string
+  | StringOptValue of string option
 
 type option_ref_value =
   | StringRefValue of string
-- 
cgit v1.2.3


From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 30 Sep 2015 22:12:25 +0200
Subject: Proof using: let-in policy, optional auto-clear, forward closure*

- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
  since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
    Set Proof Using Clear Unused.
  since clearing section hypotheses does not "always work" (e.g. hint
  databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
  theorems.
---
 intf/vernacexpr.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 9248fa953c..fd6e1c6ae1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -225,12 +225,12 @@ type scheme =
   | EqualityScheme of reference or_by_notation
 
 type section_subset_expr =
-  | SsSet of lident list
+  | SsEmpty
+  | SsSingl of lident
   | SsCompl of section_subset_expr
   | SsUnion of section_subset_expr * section_subset_expr
   | SsSubstr of section_subset_expr * section_subset_expr
-
-type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr
+  | SsFwdClose of section_subset_expr
 
 (** Extension identifiers for the VERNAC EXTEND mechanism. *)
 type extend_name =
@@ -336,7 +336,7 @@ type vernac_expr =
       class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of obsolete_locality * lident *
       class_rawexpr * class_rawexpr
-  | VernacNameSectionHypSet of lident * section_subset_descr 
+  | VernacNameSectionHypSet of lident * section_subset_expr 
 
   (* Type classes *)
   | VernacInstance of
@@ -441,7 +441,7 @@ type vernac_expr =
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard
-  | VernacProof of raw_tactic_expr option * section_subset_descr option
+  | VernacProof of raw_tactic_expr option * section_subset_expr option
   | VernacProofMode of string
   (* Toplevel control *)
   | VernacToplevelControl of exn
-- 
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.
---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index fd6e1c6ae1..f89f076b5f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -314,7 +314,7 @@ type vernac_expr =
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
-      inline * simple_binder with_coercion list
+      inline * (plident list * constr_expr) with_coercion list
   | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
-- 
cgit v1.2.3