aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--interp/modintern.ml23
-rw-r--r--intf/constrexpr.ml7
-rw-r--r--intf/vernacexpr.ml16
-rw-r--r--parsing/g_vernac.ml48
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--pretyping/univdecls.mli4
-rw-r--r--printing/ppvernac.ml4
-rw-r--r--test-suite/bugs/closed/2245.v11
-rw-r--r--test-suite/modules/WithDefUBinders.v15
-rw-r--r--toplevel/coqloop.ml20
-rw-r--r--toplevel/vernac.ml33
-rw-r--r--vernac/classes.ml36
-rw-r--r--vernac/comAssumption.mli2
-rw-r--r--vernac/comDefinition.mli4
-rw-r--r--vernac/comFixpoint.ml1
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/comInductive.mli2
20 files changed, 119 insertions, 75 deletions
diff --git a/CHANGES b/CHANGES
index 466b4cde51..ab6aab0eef 100644
--- a/CHANGES
+++ b/CHANGES
@@ -86,6 +86,8 @@ Universes
more information.
- Fix #5726: Notations that start with `Type` now support universe instances
with `@{u}`.
+- `with Definition` now understands universe declarations
+ (like `@{u| Set < u}`).
Checker
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 92264fb72b..8876855853 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -62,18 +62,19 @@ let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
let transl_with_decl env = function
| CWith_Module ((_,fqid),qid) ->
WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
- | CWith_Definition ((_,fqid),c) ->
- let sigma = Evd.from_env env in
+ | CWith_Definition ((_,fqid),udecl,c) ->
+ let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
let c, ectx = interp_constr env sigma c in
- if Flags.is_universe_polymorphism () then
- let ctx = UState.context ectx in
- let inst, ctx = Univ.abstract_universes ctx in
- let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
- let c = EConstr.to_constr sigma c in
- WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
- else
- let c = EConstr.to_constr sigma c in
- WithDef (fqid,(c, None)), UState.context_set ectx
+ begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
+ | Entries.Polymorphic_const_entry ctx ->
+ let inst, ctx = Univ.abstract_universes ctx in
+ let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
+ let c = EConstr.to_constr sigma c in
+ WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
+ | Entries.Monomorphic_const_entry ctx ->
+ let c = EConstr.to_constr sigma c in
+ WithDef (fqid,(c, None)), ctx
+ end
let loc_of_module l = l.CAst.loc
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 474b80ec48..b0a769c5a8 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -17,6 +17,11 @@ open Decl_kinds
(** [constr_expr] is the abstract syntax tree produced by the parser *)
+type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+
+type ident_decl = lident * universe_decl_expr option
+type name_decl = lname * universe_decl_expr option
+
type notation = string
type explicitation =
@@ -139,7 +144,7 @@ type constr_pattern_expr = constr_expr
type with_declaration_ast =
| CWith_Module of Id.t list Loc.located * qualid Loc.located
- | CWith_Definition of Id.t list Loc.located * constr_expr
+ | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr
type module_ast_r =
| CMident of qualid
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 7e9bc8caa9..0a6e5b3b31 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -160,11 +160,6 @@ type option_ref_value =
(** Identifier and optional list of bound universes and constraints. *)
-type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
-
-type ident_decl = lident * universe_decl_expr option
-type name_decl = lname * universe_decl_expr option
-
type sort_expr = Sorts.family
type definition_expr =
@@ -536,3 +531,14 @@ type vernac_when =
| VtNow
| VtLater
type vernac_classification = vernac_type * vernac_when
+
+
+(** Deprecated stuff *)
+type universe_decl_expr = Constrexpr.universe_decl_expr
+[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"]
+
+type ident_decl = Constrexpr.ident_decl
+[@@ocaml.deprecated "alias of Constrexpr.ident_decl"]
+
+type name_decl = Constrexpr.name_decl
+[@@ocaml.deprecated "alias of Constrexpr.name_decl"]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 595a60f335..feaef31619 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -12,10 +12,10 @@ open Pp
open CErrors
open Util
open Names
+open Vernacexpr
open Constrexpr
open Constrexpr_ops
open Extend
-open Vernacexpr
open Decl_kinds
open Declarations
open Misctypes
@@ -142,7 +142,7 @@ let name_of_ident_decl : ident_decl -> name_decl =
(* Gallina declarations *)
GEXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
- record_field decl_notation rec_definition ident_decl;
+ record_field decl_notation rec_definition ident_decl univ_decl;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
@@ -557,8 +557,8 @@ GEXTEND Gram
[ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
;
with_declaration:
- [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
- CWith_Definition (fqid,c)
+ [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
+ CWith_Definition (fqid,udecl,c)
| IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
CWith_Module (fqid,qid)
] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9aae251f1a..258c4bb11c 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -442,6 +442,7 @@ module Prim =
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
+ let univ_decl = Gram.entry_create "Prim.univ_decl"
let ident_decl = Gram.entry_create "Prim.ident_decl"
let pattern_ident = Gram.entry_create "pattern_ident"
let pattern_identref = Gram.entry_create "pattern_identref"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8592968dc1..e66aa4ade8 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -198,6 +198,7 @@ module Prim :
val ident : Id.t Gram.entry
val name : lname Gram.entry
val identref : lident Gram.entry
+ val univ_decl : universe_decl_expr Gram.entry
val ident_decl : ident_decl Gram.entry
val pattern_ident : Id.t Gram.entry
val pattern_identref : lident Gram.entry
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
index 242eb802fa..305d045b1f 100644
--- a/pretyping/univdecls.mli
+++ b/pretyping/univdecls.mli
@@ -14,8 +14,8 @@ type universe_decl =
val default_univ_decl : universe_decl
-val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr ->
+val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr ->
Evd.evar_map * universe_decl
-val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option ->
+val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option ->
Evd.evar_map * universe_decl
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 8551d040dd..2b7d643d6f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -233,9 +233,9 @@ open Decl_kinds
hov 2 (keyword "Hint "++ pph ++ opth)
let pr_with_declaration pr_c = function
- | CWith_Definition (id,c) ->
+ | CWith_Definition (id,udecl,c) ->
let p = pr_c c in
- keyword "Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p
+ keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
| CWith_Module (id,qid) ->
keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
pr_located pr_qualid qid
diff --git a/test-suite/bugs/closed/2245.v b/test-suite/bugs/closed/2245.v
new file mode 100644
index 0000000000..f0162f3b27
--- /dev/null
+++ b/test-suite/bugs/closed/2245.v
@@ -0,0 +1,11 @@
+Module Type Test.
+
+Section Sec.
+Variables (A:Type).
+Context (B:Type).
+End Sec.
+
+Fail Check B. (* used to be found !!! *)
+Fail Check A.
+
+End Test.
diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v
new file mode 100644
index 0000000000..e683455162
--- /dev/null
+++ b/test-suite/modules/WithDefUBinders.v
@@ -0,0 +1,15 @@
+
+Set Universe Polymorphism.
+Module Type T.
+ Axiom foo@{u v|u < v} : Type@{v}.
+End T.
+
+Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}.
+ Definition foo@{u v} := Type@{u} : Type@{v}.
+End M.
+
+Fail Module M' : T with Definition foo := Type.
+
+(* Without the binder expression we have to do trickery to get the
+ universes in the right order. *)
+Module M' : T with Definition foo := let t := Type in t.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 1da46e8ce6..a103cfe7f3 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -341,6 +341,22 @@ let loop_flush_all () =
Format.pp_print_flush !Topfmt.std_ft ();
Format.pp_print_flush !Topfmt.err_ft ()
+let pr_open_cur_subgoals () =
+ try
+ let proof = Proof_global.give_me_the_proof () in
+ Printer.pr_open_subgoals ~proof
+ with Proof_global.NoCurrentProof -> Pp.str ""
+
+(* Goal equality heuristic. *)
+let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
+let evleq e1 e2 = CList.equal Evar.equal e1 e2
+let cproof p1 p2 =
+ let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in
+ evleq a1 b1 &&
+ CList.equal (pequal evleq evleq) a2 b2 &&
+ CList.equal Evar.equal a3 b3 &&
+ CList.equal Evar.equal a4 b4
+
let drop_last_doc = ref None
let rec loop ~time ~state =
@@ -351,6 +367,10 @@ let rec loop ~time ~state =
(* Be careful to keep this loop tail-recursive *)
let rec vernac_loop ~state =
let nstate = do_vernac ~time ~state in
+ let proof_changed = not (Option.equal cproof nstate.proof state.proof) in
+ let print_goals = not !Flags.quiet &&
+ proof_changed && Proof_global.there_are_pending_proofs () in
+ if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
loop_flush_all ();
vernac_loop ~state:nstate
(* We recover the current stateid, threading from the caller is
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7c889500ab..56bdcc7e52 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,12 +70,6 @@ let print_cmd_header ?loc com =
Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com);
Format.pp_print_flush !Topfmt.std_ft ()
-let pr_open_cur_subgoals () =
- try
- let proof = Proof_global.give_me_the_proof () in
- Printer.pr_open_subgoals ~proof
- with Proof_global.NoCurrentProof -> Pp.str ""
-
(* Reenable when we get back to feedback printing *)
(* let is_end_of_input any = match any with *)
(* Stm.End_of_input -> true *)
@@ -94,23 +88,8 @@ end
let interp_vernac ~time ~check ~interactive ~state (loc,com) =
let open State in
try
- (* XXX: We need to run this before add as the classification is
- highly dynamic and depends on the structure of the
- document. Hopefully this is fixed when VtMeta can be removed
- and Undo etc... are just interpreted regularly. *)
-
- (* XXX: The classifier can emit warnings so we need to guard
- against that... *)
- let wflags = CWarnings.get_flags () in
- CWarnings.set_flags "none";
- let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with
- | VtProofStep _ | VtMeta | VtStartProof _ -> true
- | _ -> false
- in
- CWarnings.set_flags wflags;
-
- (* The -time option is only supported from console-based
- clients due to the way it prints. *)
+ (* The -time option is only supported from console-based clients
+ due to the way it prints. *)
if time then print_cmd_header ?loc com;
let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in
let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in
@@ -123,14 +102,6 @@ let interp_vernac ~time ~check ~interactive ~state (loc,com) =
it otherwise reveals bugs *)
(* Stm.observe nsid; *)
let ndoc = if check then Stm.finish ~doc else doc in
-
- (* We could use a more refined criteria that depends on the
- vernac. For now we imitate the old approach and rely on the
- classification. *)
- let print_goals = interactive && not !Flags.quiet &&
- is_proof_step && Proof_global.there_are_pending_proofs () in
-
- if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
let new_proof = Proof_global.give_me_the_proof_opt () in
{ doc = ndoc; sid = nsid; proof = new_proof }
with reraise ->
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 25d893bfbd..192cc8a555 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -374,16 +374,34 @@ let context poly l =
with e when CErrors.noncritical e ->
user_err Pp.(str "Anonymous variables not allowed in contexts.")
in
- let uctx = ref (Evd.universe_context_set sigma) in
+ let univs =
+ let uctx = Evd.universe_context_set sigma in
+ match ctx with
+ | [] -> assert false
+ | [_] ->
+ if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
+ else Monomorphic_const_entry uctx
+ | _::_::_ ->
+ if Lib.sections_are_opened ()
+ then
+ begin
+ Declare.declare_universe_context poly uctx;
+ if poly then Polymorphic_const_entry Univ.UContext.empty
+ else Monomorphic_const_entry Univ.ContextSet.empty
+ end
+ else if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
+ else
+ begin
+ Declare.declare_universe_context poly uctx;
+ Monomorphic_const_entry Univ.ContextSet.empty
+ end
+ in
let fn status (id, b, t) =
let b, t = Option.map (to_constr sigma) b, to_constr sigma t in
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
(* Declare the universe context once *)
- let univs = if poly
- then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
- else Monomorphic_const_entry !uctx
- in
- let () = uctx := Univ.ContextSet.empty in
let decl = match b with
| None ->
(ParameterEntry (None,(t,univs),None), IsAssumption Logical)
@@ -405,10 +423,6 @@ let context poly l =
in
let impl = List.exists test impls in
let decl = (Discharge, poly, Definitional) in
- let univs = if poly
- then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
- else Monomorphic_const_entry !uctx
- in
let nstatus = match b with
| None ->
pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
@@ -422,6 +436,4 @@ let context poly l =
in
status && nstatus
in
- if Lib.sections_are_opened () then
- Declare.declare_universe_context poly !uctx;
List.fold_left fn true (List.rev ctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index f235de3509..56e3243766 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -19,7 +19,7 @@ open Decl_kinds
(** {6 Parameters/Assumptions} *)
val do_assumptions : locality * polymorphic * assumption_object_kind ->
- Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool
+ Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
(************************************************************************)
(** Internal API *)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 0d6367291c..6f81c4575f 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,7 +17,7 @@ open Constrexpr
(** {6 Definitions/Let} *)
val do_definition : program_mode:bool ->
- Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
+ Id.t -> definition_kind -> universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
constr_expr option -> unit Lemmas.declaration_hook -> unit
@@ -27,6 +27,6 @@ val do_definition : program_mode:bool ->
(** Not used anywhere. *)
val interp_definition :
- Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
+ universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
Univdecls.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index edfe7aa819..a794c2db06 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -14,7 +14,6 @@ open Pretyping
open Evarutil
open Evarconv
open Misctypes
-open Vernacexpr
module RelDecl = Context.Rel.Declaration
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index b181984e07..36c2993afe 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -32,7 +32,7 @@ val do_cofixpoint :
type structured_fixpoint_expr = {
fix_name : Id.t;
- fix_univs : Vernacexpr.universe_decl_expr option;
+ fix_univs : Constrexpr.universe_decl_expr option;
fix_annot : Misctypes.lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 457a1da054..c59286d1a3 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -57,7 +57,7 @@ let push_types env idl tl =
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : Vernacexpr.universe_decl_expr option;
+ ind_univs : universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index b8d85c8d93..8339357246 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -47,7 +47,7 @@ val declare_mutual_inductive_with_eliminations :
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : Vernacexpr.universe_decl_expr option;
+ ind_univs : universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:35:20 +0000