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 ++--
 parsing/g_constr.ml4                  |  8 ++++----
 pretyping/detyping.ml                 |  4 ++--
 pretyping/evd.ml                      |  6 ------
 pretyping/miscops.ml                  |  2 +-
 pretyping/pretyping.ml                | 26 ++++++++++++++++++++++----
 printing/ppconstr.ml                  |  6 +++---
 test-suite/bugs/closed/3330.v         |  1 +
 test-suite/bugs/closed/3352.v         |  1 +
 test-suite/bugs/closed/3386.v         |  1 +
 test-suite/bugs/closed/3387.v         |  1 +
 test-suite/bugs/closed/3559.v         |  1 +
 test-suite/bugs/closed/3566.v         |  1 +
 test-suite/bugs/closed/3666.v         |  1 +
 test-suite/bugs/closed/3690.v         |  1 +
 test-suite/bugs/closed/3777.v         |  1 +
 test-suite/bugs/closed/3779.v         |  1 +
 test-suite/bugs/closed/3808.v         |  1 +
 test-suite/bugs/closed/3821.v         |  1 +
 test-suite/bugs/closed/3922.v         |  1 +
 test-suite/bugs/closed/4089.v         |  1 +
 test-suite/bugs/closed/4121.v         |  1 +
 test-suite/bugs/closed/4287.v         |  1 +
 test-suite/bugs/closed/4299.v         | 12 ++++++++++++
 test-suite/bugs/closed/4301.v         |  1 +
 test-suite/bugs/closed/HoTT_coq_007.v |  1 +
 test-suite/bugs/closed/HoTT_coq_036.v |  1 +
 test-suite/bugs/closed/HoTT_coq_062.v |  1 +
 test-suite/bugs/closed/HoTT_coq_093.v |  1 +
 test-suite/bugs/opened/3754.v         |  1 +
 test-suite/success/namedunivs.v       |  2 ++
 test-suite/success/polymorphism.v     |  2 ++
 test-suite/success/univnames.v        | 26 ++++++++++++++++++++++++++
 theories/Classes/CMorphisms.v         |  5 +++--
 toplevel/command.ml                   |  5 +++--
 35 files changed, 104 insertions(+), 26 deletions(-)
 create mode 100644 test-suite/bugs/closed/4299.v
 create mode 100644 test-suite/success/univnames.v

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
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e47e3fb1e6..9fe3022341 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -153,12 +153,12 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType []
-      | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u)
+      | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
       ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids
-      | id = ident -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
+      | id = identref -> [id]
       ] ]
   ;
   lconstr:
@@ -302,7 +302,7 @@ GEXTEND Gram
     [ [ "Set" -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | id = ident -> GType (Some (Id.to_string id))
+      | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
       ] ]
   ;
   fix_constr:
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8bd57290b0..a1213e72be 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -401,7 +401,7 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
+       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -413,7 +413,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
+  GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
 
 let detype_instance sigma l = 
   if Univ.Instance.is_empty l then None
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4e0b6f75e7..4372668fcf 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1074,12 +1074,6 @@ let uctx_new_univ_variable rigid name predicative
 	  uctx_univ_algebraic = Univ.LSet.add u avars}, false
 	else {uctx with uctx_univ_variables = uvars'}, false
   in
-  (* let ctx' = *)
-  (*   if pred then *)
-  (*     Univ.ContextSet.add_constraints *)
-  (* 	(Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *)
-  (*   else ctx' *)
-  (* in *)
   let names = 
     match name with
     | Some n -> add_uctx_names n u uctx.uctx_names
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 0926e7a299..a0ec1baae2 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.equal CString.equal l1 l2
+| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2efd8fe413..dec23328f4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -99,8 +99,22 @@ let search_guard loc env possible_indexes fixdefs =
 let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
 
+(* To force universe name declaration before use *)
+
+let strict_universe_declarations = ref true
+let is_strict_universe_declarations () = !strict_universe_declarations
+
+let _ =
+  Goptions.(declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "strict universe declaration";
+	    optkey   = ["Strict";"Universe";"Declaration"];
+	    optread  = is_strict_universe_declarations;
+	    optwrite = (:=) strict_universe_declarations })
+						  
 (** Miscellaneous interpretation functions *)
-let interp_universe_level_name evd s =
+let interp_universe_level_name evd (loc,s) =
   let names, _ = Universes.global_universe_names () in
     if CString.string_contains s "." then
       match List.rev (CString.split '.' s) with
@@ -122,7 +136,10 @@ let interp_universe_level_name evd s =
 	try let level = Evd.universe_of_name evd s in
 	      evd, level
 	with Not_found -> 
-	  new_univ_level_variable ~name:s univ_rigid evd
+	  if not (is_strict_universe_declarations ()) then
+  	    new_univ_level_variable ~name:s univ_rigid evd
+	  else user_err_loc (loc, "interp_universe_level_name",
+			     Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe evd = function
   | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
@@ -135,7 +152,7 @@ let interp_universe evd = function
 
 let interp_universe_level evd = function
   | None -> new_univ_level_variable univ_rigid evd
-  | Some s -> interp_universe_level_name evd s
+  | Some (loc,s) -> interp_universe_level_name evd (loc,s)
 
 let interp_sort evd = function
   | GProp -> evd, Prop Null
@@ -357,7 +374,8 @@ let evar_kind_of_term sigma c =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_universe_level_name evd = function
+let interp_universe_level_name evd l =
+  match l with
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_universe_level evd s
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 =
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index 4cd7c39e88..e6a50449da 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v
index b57b0a0f0b..f8113e4c78 100644
--- a/test-suite/bugs/closed/3352.v
+++ b/test-suite/bugs/closed/3352.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 
 (*
 I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo].  (I think this worked in HoTT/coq, too.)  Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A].  (The issue is tricker when IsHProp uses [A] elsewhere, as in:
diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v
index 0e236c2172..b8bb8bce09 100644
--- a/test-suite/bugs/closed/3386.v
+++ b/test-suite/bugs/closed/3386.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v
index ae212caa5d..cb435e7865 100644
--- a/test-suite/bugs/closed/3387.v
+++ b/test-suite/bugs/closed/3387.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index 50645090fa..da12b68689 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 8657 lines to
 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines,
 then from 51 lines to 37 lines, then from 43 lines to 30 lines *)
diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v
index b2aa8c3cd6..e2d7976981 100644
--- a/test-suite/bugs/closed/3566.v
+++ b/test-suite/bugs/closed/3566.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Notation idmap := (fun x => x).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
 Arguments idpath {A a} , [A] a.
diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v
index a5b0e9347d..e69ec10976 100644
--- a/test-suite/bugs/closed/3666.v
+++ b/test-suite/bugs/closed/3666.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index 4069e38075..df9f5f4761 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Printing Universes.
 Set Universe Polymorphism.
 Definition foo (a := Type) (b := Type) (c := Type) := Type.
diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v
index b9b2dd6b3e..e203528fcc 100644
--- a/test-suite/bugs/closed/3777.v
+++ b/test-suite/bugs/closed/3777.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Module WithoutPoly.
   Unset Universe Polymorphism.
   Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v
index eb0d206c5c..2b44e225e8 100644
--- a/test-suite/bugs/closed/3779.v
+++ b/test-suite/bugs/closed/3779.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }.
 Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T.
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
index 6e19ddf8dc..a5c84e6856 100644
--- a/test-suite/bugs/closed/3808.v
+++ b/test-suite/bugs/closed/3808.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
   := foo : Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v
index 8da4f73626..30261ed266 100644
--- a/test-suite/bugs/closed/3821.v
+++ b/test-suite/bugs/closed/3821.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .
 
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 0ccc92067d..5013bc6ac1 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Notation Type0 := Set.
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index c6cb9c35e6..e4d76732a3 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index 5f8c411ca8..d34a2b8b1b 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *)
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index e139c5b6c9..0623cf5b84 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 
 Universe b.
 
diff --git a/test-suite/bugs/closed/4299.v b/test-suite/bugs/closed/4299.v
new file mode 100644
index 0000000000..955c3017d7
--- /dev/null
+++ b/test-suite/bugs/closed/4299.v
@@ -0,0 +1,12 @@
+Unset Strict Universe Declaration.
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type : Type.
+  Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type : Type.
+  Definition U := let X := Type in Type.
+  Definition eq : Type = U := eq_refl.
+Fail End M.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v
index 3b00efb213..b4e17c2231 100644
--- a/test-suite/bugs/closed/4301.v
+++ b/test-suite/bugs/closed/4301.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 
 Module Type Foo.
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v
index 0b8bb23534..844ff87566 100644
--- a/test-suite/bugs/closed/HoTT_coq_007.v
+++ b/test-suite/bugs/closed/HoTT_coq_007.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Module Comment1.
   Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
index 4c3e078a50..7a84531a77 100644
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Module Version1.
   Set Implicit Arguments.
   Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v
index b7db22a69e..90d1d18306 100644
--- a/test-suite/bugs/closed/HoTT_coq_062.v
+++ b/test-suite/bugs/closed/HoTT_coq_062.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v
index f382dac976..4f8868d538 100644
--- a/test-suite/bugs/closed/HoTT_coq_093.v
+++ b/test-suite/bugs/closed/HoTT_coq_093.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
 Set Printing All.
 Set Printing Implicit.
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v
index 9b3f94d917..a717bbe735 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/3754.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 059462fac3..f9154ef576 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -4,6 +4,8 @@
 (* Fail  exact H. *)
 (* Section . *)
 
+Unset Strict Universe Declaration.
+
 Section lift_strict.
 Polymorphic Definition liftlt := 
   let t := Type@{i} : Type@{k} in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 957612ef1d..d6bbfe29ac 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,3 +1,5 @@
+Unset Strict Universe Declaration.
+
 Module withoutpoly.
 
 Inductive empty :=. 
diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v
new file mode 100644
index 0000000000..31d264f645
--- /dev/null
+++ b/test-suite/success/univnames.v
@@ -0,0 +1,26 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A.
+
+Set Printing Universes.
+
+Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A.
+
+Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type.
+
+Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type.
+
+Definition nothing (A : Type) := A.
+
+Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla.
+
+Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy.
+
+
+Universe g.
+
+Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9d3952e64a..fdedbf672a 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -266,8 +266,10 @@ Section GenericInstances.
     transitivity (y x0)...
   Qed.
 
+  Unset Strict Universe Declaration.
+  
   (** The complement of a crelation conserves its proper elements. *)
-  Program Definition complement_proper
+  Program Definition complement_proper (A : Type@{k}) (RA : crelation A)
           `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
     Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
   
@@ -279,7 +281,6 @@ Section GenericInstances.
   Qed.
  
   (** The [flip] too, actually the [flip] instance is a bit more general. *)
-
   Program Definition flip_proper
           `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
     Proper (RB ==> RA ==> RC) (flip f) := _.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b65ff73feb..285baf3f97 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -500,12 +500,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   let env0 = Global.env() in
-  let evdref = ref Evd.(from_env env0) in
+  let pl = (List.hd indl).ind_univs in
+  let ctx = Evd.make_evar_universe_context env0 pl in
+  let evdref = ref Evd.(from_ctx ctx) in
   let _, ((env_params, ctx_params), userimpls) =
     interp_context_evars env0 evdref paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
-  let pl = (List.hd indl).ind_univs in
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in
-- 
cgit v1.2.3


From 8a7f111ad5ce35e183016a2a968d19f29b7622c5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Oct 2015 14:32:30 +0200
Subject: Record fields accept an optional final semicolon separator.

There is no such thing as the OPTSEP macro in Camlp4 so I had
to expand it by hand.
---
 parsing/g_constr.ml4 | 22 +++++++++++++++++++---
 parsing/g_vernac.ml4 | 11 +++++++++--
 2 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9fe3022341..e2e6795f73 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -224,11 +224,20 @@ GEXTEND Gram
       ] ]
   ;
   record_declaration:
-    [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs)
+    [ [ fs = record_fields -> CRecord (!@loc, None, fs)
 (*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
 (* 	  CRecord (!@loc, Some c, fs) *)
     ] ]
   ;
+
+  record_fields:
+    [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
+      | f = record_field_declaration; ";" -> [f]
+      | f = record_field_declaration -> [f]
+      | -> []
+    ] ]
+  ;
+
   record_field_declaration:
     [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
       (id, abstract_constr_expr c (binders_of_lidents params)) ] ]
@@ -356,9 +365,16 @@ GEXTEND Gram
     [ [ pll = LIST1 mult_pattern SEP "|";
         "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
   ;
-  recordpattern:
+  record_pattern:
     [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
   ;
+  record_patterns:
+    [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps
+      | p = record_pattern; ";" -> [p]
+      | p = record_pattern-> [p]
+      | -> []
+    ] ]
+  ;
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
@@ -382,7 +398,7 @@ GEXTEND Gram
       [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
     | "0"
       [ r = Prim.reference -> CPatAtom (!@loc,Some r)
-      | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat)
+      | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
       | "_" -> CPatAtom (!@loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 63850713f2..e9915fceb3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -325,9 +325,9 @@ GEXTEND Gram
       | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
 	  Constructors ((c id)::l)
       | id = identref ; c = constructor_type -> Constructors [ c id ]
-      | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
+      | cstr = identref; "{"; fs = record_fields; "}" ->
 	  RecordDecl (Some cstr,fs)
-      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
+      | "{";fs = record_fields; "}" -> RecordDecl (None,fs)
       |  -> Constructors [] ] ]
   ;
 (*
@@ -389,6 +389,13 @@ GEXTEND Gram
   [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ];
       ntn = decl_notation -> (bd,pri),ntn ] ]
   ;
+  record_fields:
+    [ [ f = record_field; ";"; fs = record_fields -> f :: fs
+      | f = record_field; ";" -> [f]
+      | f = record_field -> [f]
+      | -> []
+    ] ]
+  ;
   record_binder_body:
     [ [ l = binders; oc = of_type_with_opt_coercion;
          t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t))
-- 
cgit v1.2.3


From 27492a7674587e1a3372cd7545e056e2775c69b3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Oct 2015 14:43:49 +0200
Subject: Test for record syntax parsing.

---
 test-suite/success/record_syntax.v | 47 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 test-suite/success/record_syntax.v

diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
new file mode 100644
index 0000000000..db2bbb0dc7
--- /dev/null
+++ b/test-suite/success/record_syntax.v
@@ -0,0 +1,47 @@
+Module A.
+
+Record Foo := { foo : unit; bar : unit }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt
+|}.
+
+Definition foo0 (p : Foo) := match p with {| |} => tt end.
+Definition foo1 (p : Foo) := match p with {| foo := f |} => f end.
+Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end.
+Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end.
+Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end.
+
+End A.
+
+Module B.
+
+Record Foo := { }.
+
+End B.
+
+Module C.
+
+Record Foo := { foo : unit; bar : unit; }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt;
+|}.
+
+End C.
+
+Module D.
+
+Record Foo := { foo : unit }.
+Definition foo_ := {| foo := tt |}.
+
+End D.
+
+Module E.
+
+Record Foo := { foo : unit; }.
+Definition foo_ := {| foo := tt; |}.
+
+End E.
-- 
cgit v1.2.3


From 08a0c44e3525d1f0c7303d189e826e25c3e3d914 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 7 Oct 2015 16:00:16 +0200
Subject: Univs: fix FingerTree contrib.

Let merge_context_set be lenient when merging the context of side
effects of an entry from solve_by_tac.
---
 pretyping/evd.ml        | 4 ++--
 pretyping/evd.mli       | 2 +-
 toplevel/obligations.ml | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4372668fcf..412fb92b3d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1028,8 +1028,8 @@ let merge_uctx sideff rigid uctx ctx' =
   let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
     { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
 
-let merge_context_set rigid evd ctx' = 
-  {evd with universes = merge_uctx false rigid evd.universes ctx'}
+let merge_context_set ?(sideff=false) rigid evd ctx' = 
+  {evd with universes = merge_uctx sideff rigid evd.universes ctx'}
 
 let merge_uctx_subst uctx s =
   { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 5a59c1776c..52d7d42120 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -542,7 +542,7 @@ val universes : evar_map -> Univ.universes
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
 val set_universe_context : evar_map -> evar_universe_context -> evar_map
 
-val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
 val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
 
 val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b942034df7..00ea2ffb84 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -796,7 +796,7 @@ let solve_by_tac name evi t poly ctx =
   let entry = Term_typing.handle_entry_side_effects env entry in
   let body, eff = Future.force entry.Entries.const_entry_body in
   assert(Declareops.side_effects_is_empty eff);
-  let ctx' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
+  let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
   (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx'
 
-- 
cgit v1.2.3


From e26b4dbedd29acbfb9cbf2320193cc68afa60cf3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 7 Oct 2015 16:51:53 +0200
Subject: Fix bug #4069: f_equal regression.

---
 plugins/cc/cctac.ml           | 17 ++++++++++-----
 test-suite/bugs/closed/4069.v | 51 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/bugs/closed/4069.v

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 6439f58d24..cbd95eaeaf 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -482,6 +482,15 @@ let congruence_tac depth l =
    This isn't particularly related with congruence, apart from
    the fact that congruence is called internally.
 *)
+    
+let new_app_global_check f args k =
+  new_app_global f args
+    (fun c ->
+     Proofview.Goal.enter
+     begin fun gl ->
+  	   let evm, _ = Tacmach.New.pf_apply type_of gl c in
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k c)
+    end)
 
 let f_equal =
   Proofview.Goal.nf_enter begin fun gl ->
@@ -490,11 +499,9 @@ let f_equal =
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         let ty = (* Termops.refresh_universes *) (type_of c1) in
-        if eq_constr_nounivs c1 c2 then Proofview.tclUNIT ()
-        else
-          Tacticals.New.tclTRY (Tacticals.New.tclTHEN
-          ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
-          (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
+        Tacticals.New.tclTHEN
+	  ((new_app_global_check _eq [|ty; c1; c2|]) Tactics.cut)
+	  (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
new file mode 100644
index 0000000000..21b03ce541
--- /dev/null
+++ b/test-suite/bugs/closed/4069.v
@@ -0,0 +1,51 @@
+
+Lemma test1 : 
+forall (v : nat) (f g : nat -> nat),
+f v = g v.
+intros. f_equal.
+(* 
+Goal in v8.5: f v = g v
+Goal in v8.4: v = v -> f v = g v
+Expected: f = g
+*)
+Admitted.
+
+Lemma test2 : 
+forall (v u : nat) (f g : nat -> nat),
+f v = g u.
+intros. f_equal.
+(* 
+In both v8.4 And v8.5
+Goal 1: v = u -> f v = g u
+Goal 2: v = u
+
+Expected Goal 1: f = g
+Expected Goal 2: v = u
+*)
+Admitted.
+
+Lemma test3 : 
+forall (v : nat) (u : list nat) (f : nat -> nat) (g : list nat -> nat),
+f v = g u.
+intros. f_equal.
+(* 
+In both v8.4 And v8.5, the goal is unchanged.
+*)
+Admitted.
+
+Require Import List.
+Lemma foo n (l k : list nat) : k ++ skipn n l = skipn n l.
+Proof. f_equal.
+(*
+  8.4: leaves the goal unchanged, i.e. k ++ skipn n l = skipn n l
+  8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l
+    and skipn n l = l
+*)
+Require Import List.
+Fixpoint replicate {A} (n : nat) (x : A) : list A :=
+  match n with 0 => nil | S n => x :: replicate n x end.
+Lemma bar {A} n m (x : A) : 
+  skipn n (replicate m x) = replicate (m - n) x ->
+  skipn n (replicate m x) = replicate (m - n) x.
+Proof. intros. f_equal.
+(* 8.5: one goal, n = m - n *)
-- 
cgit v1.2.3


From 27d4a636cb7f1fbdbced1980808a9b947405eeb5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 7 Oct 2015 23:08:45 +0200
Subject: Remove the "exists" overrides from Program. (Fix bug #4360)

---
 CHANGES                   | 2 ++
 theories/Program/Syntax.v | 7 -------
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/CHANGES b/CHANGES
index 16d86c8ff1..cf2bb49271 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,8 @@ Tactics
   "intros" automatically complete the introduction of its subcomponents, as the
   the disjunctive-conjunctive introduction patterns in non-terminal position
   already do.
+- Importing Program no longer overrides the "exists" tactic (potential source
+  of incompatibilities).
 
 API
 
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 67e9a20cc1..892305b499 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -32,10 +32,3 @@ Require List.
 Export List.ListNotations.
 
 Require Import Bvector.
-
-(** Treating n-ary exists *)
-
-Tactic Notation "exists" constr(x) := exists x.
-Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y.
-Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
-Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
-- 
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.
---
 ide/ide_slave.ml          | 4 ++++
 ide/interface.mli         | 1 +
 ide/xmlprotocol.ml        | 4 ++++
 intf/vernacexpr.mli       | 1 +
 library/goptions.ml       | 9 +++++++++
 library/goptions.mli      | 2 ++
 printing/ppvernac.ml      | 2 ++
 toplevel/vernacentries.ml | 2 ++
 8 files changed, 25 insertions(+)

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 94f9c9a361..041f2f83b8 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -291,11 +291,13 @@ let export_option_value = function
   | Goptions.BoolValue b   -> Interface.BoolValue b
   | Goptions.IntValue x    -> Interface.IntValue x
   | Goptions.StringValue s -> Interface.StringValue s
+  | Goptions.StringOptValue s -> Interface.StringOptValue s
 
 let import_option_value = function
   | Interface.BoolValue b   -> Goptions.BoolValue b
   | Interface.IntValue x    -> Goptions.IntValue x
   | Interface.StringValue s -> Goptions.StringValue s
+  | Interface.StringOptValue s -> Goptions.StringOptValue s
 
 let export_option_state s = {
   Interface.opt_sync  = s.Goptions.opt_sync;
@@ -314,6 +316,8 @@ let set_options options =
   | BoolValue b -> Goptions.set_bool_option_value name b
   | IntValue i -> Goptions.set_int_option_value name i
   | StringValue s -> Goptions.set_string_option_value name s
+  | StringOptValue (Some s) -> Goptions.set_string_option_value name s
+  | StringOptValue None -> Goptions.unset_option_value_gen None name
   in
   List.iter iter options
 
diff --git a/ide/interface.mli b/ide/interface.mli
index 464e851f6d..767c49d2bd 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -61,6 +61,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d337a911d8..84fd8929bd 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -62,10 +62,12 @@ let of_option_value = function
   | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i]
   | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b]
   | StringValue s -> constructor "option_value" "stringvalue" [of_string s]
+  | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s]
 let to_option_value = do_match "option_value" (fun s args -> match s with
   | "intvalue" -> IntValue (to_option to_int (singleton args))
   | "boolvalue" -> BoolValue (to_bool (singleton args))
   | "stringvalue" -> StringValue (to_string (singleton args))
+  | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args))
   | _ -> raise Marshal_error)
 
 let of_option_state s =
@@ -337,6 +339,8 @@ end = struct
     | IntValue None -> "none"
     | IntValue (Some i) -> string_of_int i
     | StringValue s -> s
+    | StringOptValue None -> "none"
+    | StringOptValue (Some s) -> s
     | BoolValue b -> if b then "true" else "false"
   let pr_option_state (s : option_state) =
     Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
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
diff --git a/library/goptions.ml b/library/goptions.ml
index 4f50fbfbdd..30d195f83c 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -20,6 +20,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
@@ -293,6 +294,10 @@ let declare_string_option =
   declare_option
     (fun v -> StringValue v)
     (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+let declare_stringopt_option =
+  declare_option
+    (fun v -> StringOptValue v)
+    (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
 
 (* 3- User accessible commands *)
 
@@ -324,11 +329,13 @@ let check_bool_value v = function
 
 let check_string_value v = function
   | StringValue _ -> StringValue v
+  | StringOptValue _ -> StringOptValue (Some v)
   | _ -> bad_type_error ()
 
 let check_unset_value v = function
   | BoolValue _ -> BoolValue false
   | IntValue _ -> IntValue None
+  | StringOptValue _ -> StringOptValue None
   | _ -> bad_type_error ()
 
 (* Nota: For compatibility reasons, some errors are treated as
@@ -359,6 +366,8 @@ let msg_option_value (name,v) =
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
+    | StringOptValue None   -> str"undefined"
+    | StringOptValue (Some s)   -> str s
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
diff --git a/library/goptions.mli b/library/goptions.mli
index 1c44f89081..9d87c14c50 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -128,6 +128,7 @@ type 'a write_function = 'a -> unit
 val declare_int_option   : int option option_sig -> int option write_function
 val declare_bool_option  : bool option_sig   -> bool write_function
 val declare_string_option: string option_sig -> string write_function
+val declare_stringopt_option: string option option_sig -> string option write_function
 
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
@@ -165,6 +166,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
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
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c07c756c01..5147d81bce 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1497,6 +1497,8 @@ let vernac_set_opacity locality (v,l) =
 
 let vernac_set_option locality key = function
   | StringValue s -> set_string_option_value_gen locality key s
+  | StringOptValue (Some s) -> set_string_option_value_gen locality key s
+  | StringOptValue None -> unset_option_value_gen locality key
   | IntValue n -> set_int_option_value_gen locality key n
   | BoolValue b -> set_bool_option_value_gen locality key b
 
-- 
cgit v1.2.3


From 0de499ab4702708ddfae162389617869b170c7d7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 28 Sep 2015 16:33:46 +0200
Subject: STM: fix backtrace handling

---
 stm/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 4a303f036e..ed7c234c1e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1577,7 +1577,8 @@ end = struct (* {{{ *)
       vernac_interp r_for { r_what with verbose = true };
       feedback ~state_id:r_for Feedback.Processed     
     with e when Errors.noncritical e ->
-      let msg = string_of_ppcmds (print e) in
+      let e = Errors.push e in
+      let msg = string_of_ppcmds (iprint e) in
       feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
-- 
cgit v1.2.3


From 173f07a8386bf4d3d45b49d3dc01ab047b3ad4f9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 28 Sep 2015 16:50:25 +0200
Subject: Future: make not-here/not-ready messages customizable

---
 lib/future.ml  | 20 +++++++++++++-------
 lib/future.mli |  3 +++
 2 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/lib/future.ml b/lib/future.ml
index 02d3702d77..78a158264b 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -11,21 +11,27 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t)
 let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
 let set_freeze f g = freeze := f; unfreeze := g
 
-exception NotReady of string
-exception NotHere of string
-let _ = Errors.register_handler (function
-  | NotReady name ->
+let not_ready_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
                 "asynchronous script processing and don't pass \"-quick\" to "^
-                "coqc.")
-  | NotHere name ->
+                "coqc."))
+let not_here_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
                 "asynchronous script processing and don't pass \"-quick\" to "^
-                "coqc.")
+                "coqc."))
+
+let customize_not_ready_msg f = not_ready_msg := f
+let customize_not_here_msg f = not_here_msg := f
+
+exception NotReady of string
+exception NotHere of string
+let _ = Errors.register_handler (function
+  | NotReady name -> !not_ready_msg name
+  | NotHere name -> !not_here_msg name
   | _ -> raise Errors.Unhandled)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
diff --git a/lib/future.mli b/lib/future.mli
index 324d5f7d10..de2282ae92 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
    Thy are set for the outermos layer of the system, since they have to
    deal with the whole system state. *)
 val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+
+val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
+val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
-- 
cgit v1.2.3


From f7e9e6428842dd80549a0dcd20bf872c2dd7fa8c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 30 Sep 2015 22:18:56 +0200
Subject: STM: for PIDE based UIs, edit_at requires no Reach.known_state

---
 stm/stm.ml  |  3 ++-
 stm/stm.mli | 10 ++++++----
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index ed7c234c1e..d25466e089 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2342,7 +2342,8 @@ let edit_at id =
     VCS.delete_cluster_of id;
     VCS.gc ();
     VCS.print ();
-    Reach.known_state ~cache:(interactive ()) id;
+    if not !Flags.async_proofs_full then
+      Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
diff --git a/stm/stm.mli b/stm/stm.mli
index 1d926e998e..4bad7f0a6d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -35,7 +35,9 @@ val query :
    new document tip, the document between [id] and [fo.stop] has been dropped.
    The portion between [fo.stop] and [fo.tip] has been kept.  [fo.start] is
    just to tell the gui where the editing zone starts, in case it wants to
-   graphically denote it.  All subsequent [add] happen on top of [id]. *)
+   graphically denote it.  All subsequent [add] happen on top of [id].
+   If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
+*)
 type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
 val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 
@@ -49,11 +51,11 @@ val stop_worker : string -> unit
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 
-(* Saves on the dist a .vio corresponding to the current status:
-   - if the worker prool is empty, all tasks are saved
+(* Saves on the disk a .vio corresponding to the current status:
+   - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
-     of the completed tasks is a failuere) *)
+     of the completed tasks is a failure) *)
 val snapshot_vio : DirPath.t -> string -> unit
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
-- 
cgit v1.2.3


From 188ab7f76459ab46e0ea139da8b4331d958c7102 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 5 Oct 2015 18:39:06 +0200
Subject: Spawn: use each socket exclusively for writing or reading

According to http://caml.inria.fr/mantis/view.php?id=5325
you can't use the same socket for both writing and reading.
The result is lockups (may be fixed in 4.03).
---
 lib/spawn.ml       | 44 ++++++++++++++++++++++++++++----------------
 stm/spawned.ml     | 19 ++++++++++---------
 stm/spawned.mli    |  2 +-
 toplevel/coqtop.ml |  3 ++-
 4 files changed, 41 insertions(+), 27 deletions(-)

diff --git a/lib/spawn.ml b/lib/spawn.ml
index 9b63be70aa..851c6a2235 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -45,26 +45,38 @@ end
 (* Common code *)
 let assert_ b s = if not b then Errors.anomaly (Pp.str s)
 
+(* According to http://caml.inria.fr/mantis/view.php?id=5325
+ * you can't use the same socket for both writing and reading (may change
+ * in 4.03 *)
 let mk_socket_channel () =
   let open Unix in
-  let s = socket PF_INET SOCK_STREAM 0 in
-  bind s (ADDR_INET (inet_addr_loopback,0));
-  listen s 1;
-  match getsockname s with
-  | ADDR_INET(host, port) ->
-      s, string_of_inet_addr host ^":"^ string_of_int port
+  let sr = socket PF_INET SOCK_STREAM 0 in
+  bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1;
+  let sw = socket PF_INET SOCK_STREAM 0 in
+  bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1;
+  match getsockname sr, getsockname sw with
+  | ADDR_INET(host, portr), ADDR_INET(_, portw) ->
+      (sr, sw),
+      string_of_inet_addr host
+        ^":"^ string_of_int portr ^":"^ string_of_int portw
   | _ -> assert false
 
-let accept s =
-  let r, _, _ = Unix.select [s] [] [] accept_timeout in
+let accept (sr,sw) =
+  let r, _, _ = Unix.select [sr] [] [] accept_timeout in
   if r = [] then raise (Failure (Printf.sprintf
     "The spawned process did not connect back in %2.1fs" accept_timeout));
-  let cs, _ = Unix.accept s in
-  Unix.close s;
-  let cin, cout = Unix.in_channel_of_descr cs, Unix.out_channel_of_descr cs in
+  let csr, _ = Unix.accept sr in
+  Unix.close sr;
+  let cin = Unix.in_channel_of_descr csr in
   set_binary_mode_in cin true;
+  let w, _, _ = Unix.select [sw] [] [] accept_timeout in
+  if w = [] then raise (Failure (Printf.sprintf
+    "The spawned process did not connect back in %2.1fs" accept_timeout));
+  let csw, _ = Unix.accept sw in
+  Unix.close sw;
+  let cout = Unix.out_channel_of_descr csw in
   set_binary_mode_out cout true;
-  cs, cin, cout
+  (csr, csw), cin, cout
 
 let handshake cin cout =
   try
@@ -116,7 +128,7 @@ let spawn_pipe env prog args =
   let cout = Unix.out_channel_of_descr master2worker_w in
   set_binary_mode_in cin true;
   set_binary_mode_out cout true;
-  pid, cin, cout, worker2master_r
+  pid, cin, cout, (worker2master_r, master2worker_w)
 
 let filter_args args =
   let rec aux = function
@@ -180,10 +192,10 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
 =
   let pid, oob_resp, oob_req, cin, cout, main, is_sock =
     spawn_with_control prefer_sock env prog args in
-  Unix.set_nonblock main;
+  Unix.set_nonblock (fst main);
   let gchan =
-    if is_sock then ML.async_chan_of_socket main
-    else ML.async_chan_of_file main in
+    if is_sock then ML.async_chan_of_socket (fst main)
+    else ML.async_chan_of_file (fst main) in
   let alive, watch = true, None in
   let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in
   p.watch <- Some (
diff --git a/stm/spawned.ml b/stm/spawned.ml
index a8372195d4..66fe07dbc4 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -11,7 +11,7 @@ open Spawn
 let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
 let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
 
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
 
 let handshake cin cout =
   try
@@ -26,18 +26,19 @@ let handshake cin cout =
   | End_of_file ->
       pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
 
-let open_bin_connection h p =
+let open_bin_connection h pr pw =
   let open Unix in
-  let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in
+  let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
+  let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) in
   set_binary_mode_in cin true;
   set_binary_mode_out cout true;
   let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in
   cin, cout
 
-let controller h p =
+let controller h pr pw =
   prerr_endline "starting controller thread";
   let main () =
-    let ic, oc = open_bin_connection h p in
+    let ic, oc = open_bin_connection h pr pw in
     let rec loop () =
       try
         match CThread.thread_friendly_input_value ic with
@@ -61,8 +62,8 @@ let init_channels () =
   if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
   let () = match !main_channel with
   | None -> ()
-  | Some (Socket(mh,mp)) ->
-    channels := Some (open_bin_connection mh mp);
+  | Some (Socket(mh,mpr,mpw)) ->
+    channels := Some (open_bin_connection mh mpr mpw);
   | Some AnonPipe ->
     let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
     let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
@@ -74,8 +75,8 @@ let init_channels () =
   in
   match !control_channel with
   | None -> ()
-  | Some (Socket (ch, cp)) ->
-    controller ch cp
+  | Some (Socket (ch, cpr, cpw)) ->
+    controller ch cpr cpw
   | Some AnonPipe ->
     Errors.anomaly (Pp.str "control channel cannot be a pipe")
 
diff --git a/stm/spawned.mli b/stm/spawned.mli
index d9e7baff3b..d0183e081d 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -8,7 +8,7 @@
 
 (* To link this file, threads are needed *)
 
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
 
 (* Argument parsing should set these *)
 val main_channel : chandescr option ref
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7562c29f70..9b5a09de0e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -359,7 +359,8 @@ let get_int opt n =
 
 let get_host_port opt s =
   match CString.split ':' s with
-  | [host; port] -> Some (Spawned.Socket(host, int_of_string port))
+  | [host; portr; portw] ->
+       Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
   | ["stdfds"] -> Some Spawned.AnonPipe
   | _ ->
      prerr_endline ("Error: host:port or stdfds expected after option "^opt);
-- 
cgit v1.2.3


From 27bad55f6f87af2ae3ad7921d71c02e333a853bb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 5 Oct 2015 19:02:05 +0200
Subject: CThread: blocking read + threads now works

---
 lib/cThread.ml | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

diff --git a/lib/cThread.ml b/lib/cThread.ml
index 2d1f10bf39..9cbdf5a9ea 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -8,22 +8,12 @@
 
 type thread_ic = in_channel
 
-let prepare_in_channel_for_thread_friendly_io ic =
-  Unix.set_nonblock (Unix.descr_of_in_channel ic); ic
-
-let safe_wait_timed_read fd time =
-  try Thread.wait_timed_read fd time
-  with Unix.Unix_error (Unix.EINTR, _, _) ->
-    (** On Unix, the above function may raise this exception when it is
-        interrupted by a signal. (It uses Unix.select internally.) *)
-    false
+let prepare_in_channel_for_thread_friendly_io ic = ic
 
 let thread_friendly_read_fd fd s ~off ~len =
   let rec loop () =
     try Unix.read fd s off len
-    with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) ->
-      while not (safe_wait_timed_read fd 0.05) do Thread.yield () done;
-      loop ()
+    with Unix.Unix_error(Unix.EINTR,_,_) -> loop ()
   in 
     loop ()
 
-- 
cgit v1.2.3


From 0f706b470c83a957b600496c2bca652c2cfe65e3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 7 Oct 2015 13:36:03 +0200
Subject: term_typing: strengthen discharging code

Given the way Lib.extract_hyps is coded if the const_hyps field
of a constant declaration contains a named_context that does not
have the same order of the one in Environment.env, discharging is
broken (as in some section variables are not discharged).
If const_hyps is computed by the kernel, then the order is correct by
construction.  If such list is provided by the user, the order is not
granted.

We now systematically sort the list of user provided section hyps.

The code of Proof using is building the named_context in the right
order, but the API was not enforcing/checking it.  Now it does.
---
 kernel/term_typing.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 926b387942..8eb920fb78 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -204,6 +204,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         str " " ++ str (String.conjugate_verb_to_be n) ++
         str " used but not declared:" ++
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
+  let sort evn l =
+    List.filter (fun (id,_,_) ->
+      List.exists (fun (id',_,_) -> Names.Id.equal id id') l)
+    (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map pi1 (named_context env) in
@@ -233,7 +237,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
-        declared,
+        sort env declared,
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-- 
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.
---
 doc/refman/RefMan-pro.tex        |  30 +++++--
 intf/vernacexpr.mli              |  10 +--
 kernel/term_typing.ml            |  35 ++++++--
 kernel/term_typing.mli           |   2 +-
 parsing/g_proofs.ml4             |   8 +-
 parsing/g_vernac.ml4             |  50 ++++++++----
 proofs/pfedit.mli                |   3 +-
 proofs/proof_global.ml           |  28 ++++++-
 proofs/proof_global.mli          |   6 +-
 proofs/proof_using.ml            | 172 +++++++++++++++++++--------------------
 proofs/proof_using.mli           |  15 +---
 stm/stm.ml                       |  13 ++-
 test-suite/success/proof_using.v |  76 +++++++++++++++++
 toplevel/vernacentries.ml        |  13 +--
 14 files changed, 301 insertions(+), 160 deletions(-)

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 7af87a399a..5dbf315535 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -157,6 +157,14 @@ in Section~\ref{ProofWith}.
   
   Use only section variables occurring in the statement.
 
+\variant {\tt Proof using Type*.} 
+  
+  The {\tt *} operator computes the forward transitive closure.
+  E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
+  in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
+  {\tt Type* } is the forward transitive closure of the entire set of
+  section variables occurring in the statement.
+
 \variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
   
   Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
@@ -164,14 +172,18 @@ in Section~\ref{ProofWith}.
 \variant {\tt Proof using }  {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .}
 \variant {\tt Proof using }  {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .}
 \variant {\tt Proof using }  {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using }  {\emph collection$_1$}{\tt* .}
 
-  Use section variables being in the set union or set difference of the two
-  colelctions.  See Section~\ref{Collection} to know how to form a named
+  Use section variables being, respectively, in the set union, set difference,
+  set complement, set forward transitive closure.
+  See Section~\ref{Collection} to know how to form a named
   collection.
+  The {\tt *} operator binds stronger than {\tt +} and {\tt -}.
 
 \subsubsection{{\tt Proof using} options}
-\comindex{Default Proof Using}
-\comindex{Suggest Proof Using}
+\optindex{Default Proof Using}
+\optindex{Suggest Proof Using}
+\optindex{Proof Using Clear Unused}
 
 The following options modify the behavior of {\tt Proof using}.
 
@@ -186,11 +198,17 @@ The following options modify the behavior of {\tt Proof using}.
   When {\tt Qed} is performed, suggest a {\tt using} annotation if
   the user did not provide one.
 
+\variant{\tt Unset Proof Using Clear Unused.}
+
+  When {\tt Proof using a} all section variables but for {\tt a} and
+  the variables used in the type of {\tt a} are cleared.
+  This option can be used to turn off this behavior.
+
 \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
 \comindex{Collection}\label{Collection}
 
 The command {\tt Collection} can be used to name a set of section hypotheses,
-with the purpose of making {\tt Proof using} annotations more compat.
+with the purpose of making {\tt Proof using} annotations more compact.
 
 \variant {\tt Collection Some := x y z.}
 
@@ -209,7 +227,7 @@ with the purpose of making {\tt Proof using} annotations more compat.
 \variant {\tt Collection Many := Fewer - (x y).}
 
   Define the collection named "Many" containing the set difference
-  of "Fewer" and the unamed collection {\tt x y}.
+  of "Fewer" and the unnamed collection {\tt x y}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
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
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8eb920fb78..b6df8f454b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -182,14 +182,17 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-let record_aux env s1 s2 =
+let record_aux env s_ty s_bo suggested_expr =
+  let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
-      (List.map (fun (id, _,_) -> Id.to_string id)
-        (keep_hyps env (Id.Set.union s1 s2))) in
-  Aux_file.record_in_aux "context_used" v
+      (CList.map_filter (fun (id, _,_) ->
+          if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
 
-let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
@@ -225,15 +228,17 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
                 (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
             ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
-            !suggest_proof_using kn env vars ids_typ context_ids;
+            let expr =
+              !suggest_proof_using (Constant.to_string kn)
+                env vars ids_typ context_ids in
             if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars;
+              record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.compilation_mode = Flags.BuildVo then
-          record_aux env Id.Set.empty Id.Set.empty;
+          record_aux env Id.Set.empty Id.Set.empty "";
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
@@ -307,6 +312,20 @@ let translate_local_def env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
     infer_declaration env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
+  if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
+    match def with
+    | Undef _ -> ()
+    | Def _ -> ()
+    | OpaqueDef lc ->
+       let context_ids = List.map pi1 (named_context env) in
+       let ids_typ = global_vars_set env typ in
+       let ids_def = global_vars_set env
+         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let expr =
+         !suggest_proof_using (Id.to_string id)
+           env ids_def ids_typ context_ids in
+       record_aux env ids_typ ids_def expr
+  end;
   def, typ, univs
 
 (* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea1e..8d92bcc68f 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -44,4 +44,4 @@ val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
-  (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
+  (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e254c16ba..7f5459bfa6 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -37,12 +37,12 @@ GEXTEND Gram
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
       | IDENT "Proof" ->
-          VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
+          VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; "with"; ta = tactic; 
-        l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] ->
-          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l)
-      | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr;
+        l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
         ta = OPT [ "with"; ta = tactic -> ta ] ->
           VernacProof (ta,Some l)
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e9915fceb3..fc0a4c8c31 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,7 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
 let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_descr = Gram.entry_create "vernac:section_subset_descr"
+let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
 let command_entry = ref noedit_mode
 let set_command_entry e = command_entry := e
@@ -447,20 +447,24 @@ GEXTEND Gram
   ;
 END
 
-let only_identrefs =
-  Gram.Entry.of_parser "test_only_identrefs"
+let only_starredidentrefs =
+  Gram.Entry.of_parser "test_only_starredidentrefs"
     (fun strm ->
       let rec aux n =
       match get_tok (Util.stream_nth n strm) with
         | KEYWORD "." -> ()
         | KEYWORD ")" -> ()
-        | IDENT _ -> aux (n+1)
+        | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
         | _ -> raise Stream.Failure in
       aux 0)
+let starredidentreflist_to_expr l =
+  match l with
+  | [] -> SsEmpty
+  | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
 
 (* Modules and Sections *)
 GEXTEND Gram
-  GLOBAL: gallina_ext module_expr module_type section_subset_descr;
+  GLOBAL: gallina_ext module_expr module_type section_subset_expr;
 
   gallina_ext:
     [ [ (* Interactive module declaration *)
@@ -483,7 +487,7 @@ GEXTEND Gram
       | IDENT "End"; id = identref -> VernacEndSegment id
 
       (* Naming a set of section hyps *)
-      | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
+      | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
           VernacNameSectionHypSet (id, expr)
 
       (* Requiring an already compiled module *)
@@ -574,22 +578,32 @@ GEXTEND Gram
           CMwith (!@loc,mty,decl)
       ] ]
   ;
-  section_subset_descr:
-    [ [ IDENT "All" -> SsAll
-      | "Type" -> SsType
-      | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
-      | e = section_subset_expr -> SsExpr e ] ]
-  ;
+  (* Proof using *)
   section_subset_expr:
+    [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+          starredidentreflist_to_expr l
+      | e = ssexpr -> e ]]
+  ;
+  starredidentref:
+    [ [ i = identref -> SsSingl i
+      | i = identref; "*" -> SsFwdClose(SsSingl i)
+      | "Type" -> SsSingl (!@loc, Id.of_string "Type")
+      | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+  ;
+  ssexpr:
     [ "35" 
-      [ "-"; e = section_subset_expr -> SsCompl e ]
+      [ "-"; e = ssexpr -> SsCompl e ]
     | "50"
-      [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
-      | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
+      [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
+      | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
     | "0"
-      [ i = identref -> SsSet [i]
-      | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
-      | "("; e = section_subset_expr; ")"-> e ] ]
+      [ i = starredidentref -> i
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+          starredidentreflist_to_expr l
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+          SsFwdClose(starredidentreflist_to_expr l)
+      | "("; e = ssexpr; ")"-> e 
+      | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
   ;
 END
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 4aa3c3bfd2..b1fba132d9 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -117,7 +117,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit
 (** {6 ... } *)
 (** [set_used_variables l] declares that section variables [l] will be
     used in the proof *)
-val set_used_variables : Id.t list -> Context.section_context
+val set_used_variables :
+  Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
 (** {6 ... } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 254aa8f783..f777e6ed7a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -250,17 +250,43 @@ let start_dependent_proof id str goals terminator =
 
 let get_used_variables () = (cur_pstate ()).section_vars
 
+let proof_using_auto_clear = ref true
+let _ = Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Proof using Clear Unused";
+      Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
+      Goptions.optread  = (fun () -> !proof_using_auto_clear);
+      Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
+
 let set_used_variables l =
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe, to_clear as orig) =
+    match entry with
+    | (x,None,_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
+    | (x,Some bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe, to_clear)
+       else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+  let ctx, _, to_clear =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
+  let to_clear = if !proof_using_auto_clear then to_clear else [] in
   match !pstates with
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
         Errors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest;
-      ctx
+      ctx, to_clear
 
 let get_open_goals () =
   let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index b5dd5ef85f..028116049c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -129,8 +129,10 @@ val set_interp_tac :
     -> unit
 
 (** Sets the section variables assumed by the proof, returns its closure
- * (w.r.t. type dependencies *)
-val set_used_variables : Names.Id.t list -> Context.section_context
+ * (w.r.t. type dependencies and let-ins covered by it) + a list of
+ * ids to be cleared *)
+val set_used_variables :
+  Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
 (**********************************************************)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f66e965712..7eed1cb317 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -11,20 +11,15 @@ open Environ
 open Util
 open Vernacexpr
 
-let to_string = function
-  | SsAll -> "All"
-  | SsType -> "Type"
-  | SsExpr(SsSet l)-> String.concat " " (List.map Id.to_string (List.map snd l))
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet [] -> "( )"
-        | SsSet [_,x] -> Id.to_string x
-        | SsSet l ->
-          "(" ^ String.concat " " (List.map Id.to_string (List.map snd l)) ^ ")"
-        | SsCompl e -> "-" ^ aux e^""
-        | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
-        | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
-      in aux e
+let to_string e =
+  let rec aux = function
+    | SsEmpty -> "()"
+    | SsSingl (_,id) -> "("^Id.to_string id^")"
+    | SsCompl e -> "-" ^ aux e^""
+    | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
+    | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
+    | SsFwdClose e -> "("^aux e^")*"
+  in aux e
 
 let known_names = Summary.ref [] ~name:"proofusing-nameset"
 
@@ -36,30 +31,48 @@ let in_nameset =
     discharge_function = (fun _ -> None)
   }
 
+let rec close_fwd e s =
+  let s' =
+    List.fold_left (fun s (id,b,ty) ->      
+      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
+      let vty = global_vars_set e ty in
+      let vbty = Id.Set.union vb vty in
+      if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
+      then Id.Set.add id (Id.Set.union s vbty) else s)
+    s (named_context e)
+    in
+  if Id.Set.equal s s' then s else close_fwd e s'
+;;
+
 let rec process_expr env e ty =
-  match e with
-  | SsAll ->
-      List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet l -> set_of_list env (List.map snd l)
-        | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
-        | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
-        | SsCompl e -> Id.Set.diff (full_set env) (aux e)
-      in
-        aux e
-  | SsType ->
-      List.fold_left (fun acc ty ->
+  let rec aux = function
+    | SsEmpty -> Id.Set.empty
+    | SsSingl (_,id) -> set_of_id env ty id
+    | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
+    | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
+    | SsCompl e -> Id.Set.diff (full_set env) (aux e)
+    | SsFwdClose e -> close_fwd env (aux e)
+  in
+    aux e
+
+and set_of_id env ty id =
+  if Id.to_string id = "Type" then
+    List.fold_left (fun acc ty ->
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
-and set_of_list env = function
-  | [x] when CList.mem_assoc_f Id.equal x !known_names ->
-      process_expr env (CList.assoc_f Id.equal x !known_names) []
-  | l -> List.fold_right Id.Set.add l Id.Set.empty
-and full_set env = set_of_list env (List.map pi1 (named_context env))
+  else if Id.to_string id = "All" then
+    List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+  else if CList.mem_assoc_f Id.equal id !known_names then
+    process_expr env (CList.assoc_f Id.equal id !known_names) []
+  else Id.Set.singleton id
+
+and full_set env =
+  List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
-  let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in
+  let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
+  let v_ty = process_expr env ty_expr ty in
+  let s = Id.Set.union v_ty (process_expr env e ty) in
   Id.Set.elements s
 
 let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
@@ -77,62 +90,49 @@ let minimize_hyps env ids =
   in
     aux ids
 
-let minimize_unused_hyps env ids =
-  let all_ids = List.map pi1 (named_context env) in
-  let deps_of =
-    let cache =
-      List.map (fun id -> id,really_needed env (Id.Set.singleton id)) all_ids in
-    fun id -> List.assoc id cache in
-  let inv_dep_of =
-    let cache_sum cache id stuff =
-      try Id.Map.add id (Id.Set.add stuff (Id.Map.find id cache)) cache
-      with Not_found -> Id.Map.add id (Id.Set.singleton stuff) cache in
-    let cache =
-      List.fold_left (fun cache id ->
-        Id.Set.fold (fun d cache -> cache_sum cache d id)
-          (Id.Set.remove id (deps_of id)) cache)
-        Id.Map.empty all_ids in
-    fun id -> try Id.Map.find id cache with Not_found -> Id.Set.empty in
-  let rec aux s =
-    let s' =
-      Id.Set.fold (fun id s ->
-        if Id.Set.subset (inv_dep_of id) s then Id.Set.diff s (inv_dep_of id)
-        else s)
-      s s in
-    if Id.Set.equal s s' then s else aux s' in
-  aux ids
-
-let suggest_Proof_using kn env vars ids_typ context_ids =
+let remove_ids_and_lets env s ids =
+  let not_ids id = not (Id.Set.mem id ids) in
+  let no_body id = named_body id env = None in
+  let deps id = really_needed env (Id.Set.singleton id) in
+    (Id.Set.filter (fun id ->
+      not_ids id &&
+     (no_body id ||
+       Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
+
+let suggest_Proof_using name env vars ids_typ context_ids =
   let module S = Id.Set in
   let open Pp in
-  let used = S.union vars ids_typ in
-  let needed = minimize_hyps env used in
-  let all_needed = really_needed env needed in
-  let all = List.fold_right S.add context_ids S.empty in
-  let unneeded = minimize_unused_hyps env (S.diff all needed) in
-  let pr_set s =
+  let print x = prerr_endline (string_of_ppcmds x) in
+  let pr_set parens s =
     let wrap ppcmds =
-      if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All"))
-      then str "(" ++ ppcmds ++ str ")"
+      if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
       else ppcmds in
     wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
+  let used = S.union vars ids_typ in
+  let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
+  let all_needed = really_needed env needed in
+  let all = List.fold_right S.add context_ids S.empty in
+  let fwd_typ = close_fwd env ids_typ in
   if !Flags.debug then begin
-    prerr_endline (string_of_ppcmds (str "All " ++ pr_set all));
-    prerr_endline (string_of_ppcmds (str "Type" ++ pr_set ids_typ));
-    prerr_endline (string_of_ppcmds (str "needed " ++ pr_set needed));
-    prerr_endline (string_of_ppcmds (str "unneeded " ++ pr_set unneeded));
+    print (str "All "        ++ pr_set false all);
+    print (str "Type "       ++ pr_set false ids_typ);
+    print (str "needed "     ++ pr_set false needed);
+    print (str "all_needed " ++ pr_set false all_needed);
+    print (str "Type* "      ++ pr_set false fwd_typ);
   end;
+  let valid_exprs = ref [] in
+  let valid e = valid_exprs := e :: !valid_exprs in
+  if S.is_empty needed then valid (str "Type");
+  if S.equal all_needed fwd_typ then valid (str "Type*");
+  if S.equal all all_needed then valid(str "All");
+  valid (pr_set false needed);
   msg_info (
-    str"The proof of "++
-    Names.Constant.print kn ++ spc() ++ str "should start with:"++spc()++
-    str"Proof using " ++
-    if S.is_empty needed then str "."
-    else if S.subset needed ids_typ then str "Type."
-    else if S.equal all all_needed then str "All."
-    else 
-      let s1 = string_of_ppcmds (str "-" ++ pr_set unneeded ++ str".") in
-      let s2 = string_of_ppcmds (pr_set needed ++ str".") in
-      if String.length s1 < String.length s2 then str s1 else str s2)
+    str"The proof of "++ str name ++ spc() ++
+    str "should start with one of the following commands:"++spc()++
+    v 0 (
+    prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
+  string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs)
+;;
 
 let value = ref false
 
@@ -146,13 +146,13 @@ let _ =
       Goptions.optwrite = (fun b ->
         value := b;
         if b then Term_typing.set_suggest_proof_using suggest_Proof_using
-        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> ())
+        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
       ) }
 
-let value = ref "_unset_"
+let value = ref None
 
 let _ =
-  Goptions.declare_string_option
+  Goptions.declare_stringopt_option
     { Goptions.optsync  = true;
       Goptions.optdepr  = false;
       Goptions.optname  = "default value for Proof using";
@@ -161,6 +161,4 @@ let _ =
       Goptions.optwrite = (fun b -> value := b;) }
 
 
-let get_default_proof_using () =
-  if !value = "_unset_" then None
-  else Some !value
+let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index fb3497f106..dcf8a0fcd2 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,21 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-(* [minimize_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and [keep_hyps e s1] is equal to [keep_hyps e s2].  Inefficient. *)
-val minimize_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
-(* [minimize_unused_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and s.t. calling [clear s1] would do the same as [clear s2].  Inefficient. *)
-val minimize_unused_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
 val process_expr :
-  Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list ->
+  Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
     Names.Id.t list
 
-val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit
+val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
-val to_string : Vernacexpr.section_subset_descr -> string
+val to_string : Vernacexpr.section_subset_expr -> string
 
 val get_default_proof_using : unit -> string option
diff --git a/stm/stm.ml b/stm/stm.ml
index d25466e089..acbb5f646d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -888,9 +888,16 @@ let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
 let get_hint_ctx loc =
   let s = Aux_file.get !hints loc "context_used" in
-  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
-  let ids = List.map (fun id -> Loc.ghost, id) ids in
-  SsExpr (SsSet ids)
+  match Str.split (Str.regexp ";") s with
+  | ids :: _ ->
+      let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
+      let ids = List.map (fun id -> Loc.ghost, id) ids in
+      begin match ids with
+      | [] -> SsEmpty
+      | x :: xs ->
+          List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
+      end
+  | _ -> raise Not_found
 
 let get_hint_bp_time proof_name =
   try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index 61e73f8587..c83f45e2a4 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -117,5 +117,81 @@ End T1.
 
 Check (bla 7 : 2 = 8).
 
+Section A.
+Variable a : nat.
+Variable b : nat.
+Variable c : nat.
+Variable H1 : a = 3.
+Variable H2 : a = 3 -> b = 7.
+Variable H3 : c = 3.
+
+Lemma foo : a = a.
+Proof using Type*.
+pose H1 as e1.
+pose H2 as e2.
+reflexivity.
+Qed.
+
+Lemma bar : a = 3 -> b = 7.
+Proof using b*.
+exact H2.
+Qed.
+
+Lemma baz : c=3.
+Proof using c*.
+exact H3.
+Qed.
+
+Lemma baz2 : c=3.
+Proof using c* a.
+exact H3.
+Qed.
+
+End A.
+
+Check (foo 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (bar 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (baz2 99 3 (refl_equal 3)).
+Check (baz 3 (refl_equal 3)).
+
+Section Let.
+
+Variables a b : nat.
+Let pa : a = a. Proof. reflexivity. Qed.
+Unset Default Proof Using.
+Set Suggest Proof Using.
+Lemma test_let : a = a.
+Proof using a.
+exact pa.
+Qed.
+
+Let ppa : pa = pa. Proof. reflexivity. Qed.
+
+Lemma test_let2 : pa = pa.
+Proof using Type.
+exact ppa.
+Qed.
+
+End Let.
+
+Check (test_let 3).
+
+Section Clear.
+
+Variable a: nat.
+Hypotheses H : a = 4.
+
+Set Proof Using Clear Unused.
+
+Lemma test_clear : a = a.
+Proof using a.
+Fail rewrite H.
+trivial.
+Qed.
+
+End Clear.
+
 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5147d81bce..72c800f0f1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -874,18 +874,7 @@ let vernac_set_used_variables e =
       errorlabstrm "vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
-  let closure_l = List.map pi1 (set_used_variables l) in
-  let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in
-  let vars_of = Environ.global_vars_set in
-  let aux env entry (all_safe,rest as orig) =
-    match entry with
-    | (x,None,_) ->
-       if Id.Set.mem x all_safe then orig else (all_safe, (Loc.ghost,x)::rest) 
-    | (x,Some bo, ty) ->
-       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
-       if Id.Set.subset vars all_safe then (Id.Set.add x all_safe, rest)
-       else (all_safe, (Loc.ghost,x) :: rest) in
-  let _,to_clear = Environ.fold_named_context aux env ~init:(closure_l,[]) in
+  let _, to_clear = set_used_variables l in
   vernac_solve
     SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false
 
-- 
cgit v1.2.3


From 4a0fd14dcae807e0e681cfc14daca978cb4a36e9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Oct 2015 16:43:50 +0200
Subject: aux_file: export API to ease writing of a Proof Using annotator.

---
 lib/aux_file.ml           |  2 ++
 lib/aux_file.mli          |  4 ++++
 toplevel/vernacentries.ml | 22 +++++++++++++++-------
 3 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c9018c9ee9..5dedb0d0ac 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -42,6 +42,8 @@ module M = Map.Make(String)
 type data = string M.t
 type aux_file = data H.t
 
+let contents x = x
+
 let empty_aux_file = H.empty
 
 let get aux loc key = M.find key (H.find (Loc.unloc loc) aux)
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index e340fc6547..b672d3db28 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string
 val empty_aux_file : aux_file
 val set : aux_file -> Loc.t -> string -> string -> aux_file
 
+module H : Map.S with type key = int * int
+module M : Map.S with type key = string
+val contents : aux_file -> string M.t H.t
+
 val start_aux_file_for : string -> unit
 val stop_aux_file : unit -> unit 
 val recording : unit -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 72c800f0f1..6f1ed85e07 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1846,8 +1846,9 @@ let vernac_load interp fname =
 
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
- * still parsed as the obsolete_locality grammar entry for retrocompatibility *)
-let interp ?proof locality poly c =
+ * still parsed as the obsolete_locality grammar entry for retrocompatibility.
+ * loc is the Loc.t of the vernacular command being interpreted. *)
+let interp ?proof ~loc locality poly c =
   prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
   match c with
   (* Done later in this file *)
@@ -1991,10 +1992,16 @@ let interp ?proof locality poly c =
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) -> ()
-  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
-  | VernacProof (None, Some l) -> vernac_set_used_variables l
+  | VernacProof (None, None) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no"
+  | VernacProof (Some tac, None) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no";
+      vernac_set_end_tac tac
+  | VernacProof (None, Some l) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes";
+      vernac_set_used_variables l
   | VernacProof (Some tac, Some l) -> 
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes";
       vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
   (* Toplevel control *)
@@ -2146,8 +2153,9 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         Obligations.set_program_mode isprogcmd;
         try
           vernac_timeout begin fun () ->
-          if verbosely then Flags.verbosely (interp ?proof locality poly) c
-                       else Flags.silently  (interp ?proof locality poly) c;
+          if verbosely
+            then Flags.verbosely (interp ?proof ~loc locality poly) c
+            else Flags.silently  (interp ?proof ~loc locality poly) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
             Flags.program_mode := orig_program_mode
           end
-- 
cgit v1.2.3


From 479d45e679e8486c65b77f2ddfa8718c24778a75 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 Oct 2015 11:00:22 +0200
Subject: f_equal fix continued: do a refresh_universes as before.

---
 plugins/cc/cctac.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index cbd95eaeaf..068cb25cf2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -483,24 +483,26 @@ let congruence_tac depth l =
    the fact that congruence is called internally.
 *)
     
-let new_app_global_check f args k =
-  new_app_global f args
-    (fun c ->
-     Proofview.Goal.enter
-     begin fun gl ->
-  	   let evm, _ = Tacmach.New.pf_apply type_of gl c in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k c)
+let mk_eq f c1 c2 k =
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+  Proofview.Goal.enter begin
+    fun gl ->
+    let open Tacmach.New in
+    let evm, ty = pf_apply type_of gl c1 in
+    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
+    let term = mkApp (fc, [| ty; c1; c2 |]) in
+    let evm, _ =  type_of (pf_env gl) evm term in
+    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
+			  (k term)
     end)
-
+    
 let f_equal =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
-        let ty = (* Termops.refresh_universes *) (type_of c1) in
         Tacticals.New.tclTHEN
-	  ((new_app_global_check _eq [|ty; c1; c2|]) Tactics.cut)
+	  (mk_eq _eq c1 c2 Tactics.cut)
 	  (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
-- 
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 +-
 parsing/g_vernac.ml4      |  2 +-
 printing/ppvernac.ml      | 12 +++++++-----
 stm/texmacspp.ml          |  5 +++--
 stm/vernac_classifier.ml  |  2 +-
 toplevel/command.ml       | 40 +++++++++++++++++++++++++++++++++++++++-
 toplevel/command.mli      |  2 +-
 toplevel/vernacentries.ml |  2 +-
 8 files changed, 54 insertions(+), 13 deletions(-)

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
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fc0a4c8c31..3bd190bb8a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -420,7 +420,7 @@ GEXTEND Gram
     [ [ "("; a = simple_assum_coe; ")" -> a ] ]
   ;
   simple_assum_coe:
-    [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
+    [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr ->
         (not (Option.is_empty oc),(idl,c)) ] ]
   ;
 
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" " ++
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index fb41bb7bea..b912080413 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -575,10 +575,11 @@ let rec tmpp v loc =
       end
   | VernacExactProof _ as x -> xmlTODO loc x
   | VernacAssumption ((l, a), _, sbwcl) ->
+      let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
       let many =
-        List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in
+        List.length (List.flatten (List.map fst binders)) > 1 in
       let exprs =
-        List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in
+        List.flatten (List.map pp_simple_binder binders) in
       let l = match l with Some x -> x | None -> Decl_kinds.Global in
       let kind = string_of_assumption_kind l a many in
       xmlAssumption kind loc exprs
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 8aa2a59177..a898c687be 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -141,7 +141,7 @@ let rec classify_vernac e =
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
-        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
+        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
         VtSideff ids, VtLater    
     | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
     | VernacInductive (_,_,l) ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 285baf3f97..e54a82c19b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -251,7 +251,7 @@ let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl =
   in
   List.rev refs, status
 
-let do_assumptions (_, poly, _ as kind) nl l =
+let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
   let env = Global.env () in
   let evdref = ref (Evd.from_env env) in
   let l = 
@@ -284,6 +284,44 @@ let do_assumptions (_, poly, _ as kind) nl l =
     in
       (subst'@subst, status' && status)) ([],true) l)
 
+let do_assumptions_bound_univs coe kind nl id pl c =
+  let env = Global.env () in
+  let ctx = Evd.make_evar_universe_context env pl in
+  let evdref = ref (Evd.from_ctx ctx) in
+  let ty, impls = interp_type_evars_impls env evdref c in
+  let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+  let ty = nf ty in
+  let vars = Universes.universes_of_constr ty in
+  let evd = Evd.restrict_universe_context !evdref vars in
+  let uctx = Evd.universe_context ?names:pl evd in
+  let uctx = Univ.ContextSet.of_context uctx in
+  let (_, _, st) = declare_assumption coe kind (ty, uctx) impls false nl id in
+  st
+
+let do_assumptions kind nl l = match l with
+| [coe, ([id, Some pl], c)] ->
+  let () = match kind with
+  | (Discharge, _, _) when Lib.sections_are_opened () ->
+    let loc = fst id in
+    let msg = Pp.str "Section variables cannot be polymorphic." in
+    user_err_loc (loc, "", msg)
+  | _ -> ()
+  in
+  do_assumptions_bound_univs coe kind nl id (Some pl) c
+| _ ->
+  let map (coe, (idl, c)) =
+    let map (id, univs) = match univs with
+    | None -> id
+    | Some _ ->
+      let loc = fst id in
+      let msg = Pp.str "Assumptions with bound universes can only be defined once at a time." in
+      user_err_loc (loc, "", msg)
+    in
+    (coe, (List.map map idl, c))
+  in
+  let l = List.map map l in
+  do_assumptions_unbound_univs kind nl l
+
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
 (* 3b| Mutual inductive definitions *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index f4d43ec533..b1e1d7d060 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -57,7 +57,7 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   global_reference * Univ.Instance.t * bool
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> simple_binder with_coercion list -> bool
+  Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
 
 (* val declare_assumptions : variable Loc.located list -> *)
 (*   coercion_flag -> assumption_kind -> types Univ.in_universe_context_set ->  *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6f1ed85e07..820903c417 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -515,7 +515,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let kind = local, poly, kind in
   List.iter (fun (is_coe,(idl,c)) ->
     if Dumpglob.dump () then
-      List.iter (fun lid ->
+      List.iter (fun (lid, _) ->
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
   let status = do_assumptions kind nl l in
-- 
cgit v1.2.3


From d6ff0fcefa21bd2c6424627049b0f5e49ed4df12 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 Oct 2015 14:58:11 +0200
Subject: Univs: fix bug #4161.

Retypecheck abstracted infered predicate to register the right
universe constraints.
---
 pretyping/cases.ml            | 32 ++++++++++++++++----------------
 test-suite/bugs/closed/4161.v | 27 +++++++++++++++++++++++++++
 2 files changed, 43 insertions(+), 16 deletions(-)
 create mode 100644 test-suite/bugs/closed/4161.v

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 05e09b9686..2a4be9f31c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1865,7 +1865,14 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
+let context_of_arsign l =
+  let (x, _) = List.fold_right
+    (fun c (x, n) ->
+       (lift_rel_context n c @ x, List.length c + n))
+    l ([], 0)
+  in x
+
+let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
   let subst, len =
     List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
@@ -1905,7 +1912,9 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
 	      mkRel (n + nar))
       | _ ->
 	  map_constr_with_binders succ predicate lift c
-  in predicate 0 c
+  in
+  let p = predicate 0 c in
+  fst (Typing.type_of (push_rel_context (context_of_arsign arsign) env) sigma p), p
 
 
 (* Builds the predicate. If the predicate is dependent, its context is
@@ -1927,11 +1936,11 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
 	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let pred1 =
-          prepare_predicate_from_arsign_tycon loc tomatchs arsign t in
+        let sigma1,pred1 =
+          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	[sigma, pred1; sigma2, pred2]
+	[sigma1, pred1; sigma2, pred2]
     | None, _ ->
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
@@ -2366,13 +2375,6 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
     assert(Int.equal slift 0); (* we must have folded over all elements of the arity signature *)
     arsign'', allnames, nar, eqs, neqs, refls
 
-let context_of_arsign l =
-  let (x, _) = List.fold_right
-    (fun c (x, n) ->
-       (lift_rel_context n c @ x, List.length c + n))
-    l ([], 0)
-  in x
-
 let compile_program_cases loc style (typing_function, evdref) tycon env
     (predopt, tomatchl, eqns) =
   let typing_fun tycon env = function
@@ -2404,10 +2406,8 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
     | Some t ->
 	let pred = 
 	  try
-	    let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in
-	      (* The tycon may be ill-typed after abstraction. *)
-	    let env' = push_rel_context (context_of_arsign sign) env in
-	      ignore(Typing.sort_of env' evdref pred); pred
+	    let evd, pred = prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t in
+	      evdref := evd; pred
 	  with e when Errors.noncritical e ->
 	    let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
 	      lift nar t
diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v
new file mode 100644
index 0000000000..aa2b189b67
--- /dev/null
+++ b/test-suite/bugs/closed/4161.v
@@ -0,0 +1,27 @@
+
+    (* Inductive t : Type -> Type := *)
+    (* | Just : forall (A : Type), t A -> t A. *)
+
+    (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *)
+    (*   match x in t A return t (A + unit) with *)
+    (*   | Just T x => @test T x *)
+    (*   end. *)
+
+
+    Definition Type1 := Type.
+Definition Type2 := Type.
+Definition cast (x:Type2) := x:Type1.
+Axiom f: Type2 -> Prop.
+Definition A :=
+ let T := fun A:Type1 => _ in
+ fun A':Type2 =>
+ eq_refl : T A' = f A' :> Prop.
+(* Type2 <= Type1... f A -> Type1 <= Type2 *)
+
+Inductive t : Type -> Type :=
+    | Just : forall (A : Type), t A -> t A.
+
+Fixpoint test {A : Type} (x : t A) : t (A + unit) :=
+  match x in t A with
+  | Just B x => @test B x
+  end.
\ No newline at end of file
-- 
cgit v1.2.3


From dbdef043ea143f871a3710bae36dfc45fd815835 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 Oct 2015 13:47:05 +0200
Subject: Allowing empty bound universe variables.

---
 parsing/g_vernac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3bd190bb8a..1f9f57f698 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -269,7 +269,7 @@ GEXTEND Gram
       | -> NoInline] ]
   ;
   pidentref:
-    [ [ i = identref; l = OPT [ "@{" ; l = LIST1 identref; "}" -> l ] -> (i,l) ] ]
+    [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
   ;
   univ_constraint:
     [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
-- 
cgit v1.2.3


From b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 Oct 2015 16:00:06 +0200
Subject: Univs: fix bug #3807

Add a flag to disallow minimization to set
---
 kernel/univ.ml         |  3 +++
 kernel/univ.mli        |  1 +
 library/universes.ml   | 11 ++++++++++-
 library/universes.mli  |  3 +++
 pretyping/evd.ml       |  3 +--
 pretyping/pretyping.ml |  9 +++++++++
 6 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 34eb283d73..c0bd3bacd7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1797,6 +1797,9 @@ struct
   let empty = (LSet.empty, Constraint.empty)
   let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
 
+  let equal (univs, cst as x) (univs', cst' as y) =
+    x == y || (LSet.equal univs univs' && Constraint.equal cst cst')
+									
   let of_set s = (s, Constraint.empty)
   let singleton l = of_set (LSet.singleton l)
   let of_instance i = of_set (Instance.levels i)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4cc8a2528f..cbaf7e546a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -360,6 +360,7 @@ sig
   val of_instance : Instance.t -> t
   val of_set : universe_set -> t
 
+  val equal : t -> t -> bool
   val union : t -> t -> t
 
   val append : t -> t -> t
diff --git a/library/universes.ml b/library/universes.ml
index bc42cc044c..0656188eb5 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -26,6 +26,11 @@ let pr_with_global_universes l =
   try Nameops.pr_id (LMap.find l (snd !global_universes))
   with Not_found -> Level.pr l
 
+(* To disallow minimization to Set *)
+
+let set_minimization = ref true
+let is_set_minimization () = !set_minimization
+			    
 type universe_constraint_type = ULe | UEq | ULub
 
 type universe_constraint = universe * universe_constraint_type * universe
@@ -832,7 +837,9 @@ let normalize_context_set ctx us algs =
     Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
         if d == Le then
 	  if Univ.Level.is_small l then
-	    (Constraint.add cstr smallles, noneqs)
+	    if is_set_minimization () then
+	      (Constraint.add cstr smallles, noneqs)
+	    else (smallles, noneqs)
 	  else if Level.is_small r then
 	    if Level.is_prop r then
 	      raise (Univ.UniverseInconsistency
@@ -872,6 +879,8 @@ let normalize_context_set ctx us algs =
       if d == Eq then (UF.union l r uf; noneqs)
       else (* We ignore the trivial Prop/Set <= i constraints. *)
 	if d == Le && Univ.Level.is_small l then noneqs
+	else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r
+	then noneqs
 	else Constraint.add cstr noneqs)
       csts Constraint.empty
   in
diff --git a/library/universes.mli b/library/universes.mli
index 5527da0903..4ff21d45c9 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -12,6 +12,9 @@ open Term
 open Environ
 open Univ
 
+val set_minimization : bool ref
+val is_set_minimization : unit -> bool
+       
 (** Universes *)
 
 type universe_names = 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 412fb92b3d..3d912ca4ce 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1324,8 +1324,7 @@ let normalize_evar_universe_context uctx =
       Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
         uctx.uctx_univ_algebraic
     in
-      if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then 
-        uctx
+      if Univ.ContextSet.equal us' uctx.uctx_local then uctx
       else
 	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
 	let uctx' = 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dec23328f4..6306739b7a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -112,6 +112,15 @@ let _ =
 	    optkey   = ["Strict";"Universe";"Declaration"];
 	    optread  = is_strict_universe_declarations;
 	    optwrite = (:=) strict_universe_declarations })
+
+let _ =
+  Goptions.(declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "minimization to Set";
+	    optkey   = ["Universe";"set";"Minimization"];
+	    optread  = Universes.is_set_minimization;
+	    optwrite = (:=) Universes.set_minimization })
 						  
 (** Miscellaneous interpretation functions *)
 let interp_universe_level_name evd (loc,s) =
-- 
cgit v1.2.3


From 73daf37ccc7a44cd29c9b67405111756c75cb26a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 9 Oct 2015 09:48:48 +0200
Subject: Remove misleading warning (Close #4365)

---
 proofs/proof_global.ml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f777e6ed7a..3e06294e64 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -365,10 +365,6 @@ type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.ev
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
-  if Proof.is_complete proof then begin
-    msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++
-     str" is complete, no need to end it with Admitted");
-  end;
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in
   let eff = Evd.eval_side_effects evd in
-- 
cgit v1.2.3