aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--printing/ppvernac.ml12
-rw-r--r--stm/texmacspp.ml5
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--toplevel/command.ml40
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/vernacentries.ml2
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:08:54 +0000