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.

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