aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES.md9
-rw-r--r--clib/dyn.ml22
-rw-r--r--clib/dyn.mli6
-rw-r--r--clib/store.ml83
-rw-r--r--clib/store.mli9
-rw-r--r--doc/sphinx/language/gallina-extensions.rst6
-rw-r--r--gramlib/grammar.ml13
-rw-r--r--gramlib/grammar.mli1
-rw-r--r--kernel/uGraph.ml16
-rw-r--r--kernel/uGraph.mli2
-rw-r--r--parsing/pcoq.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml12
-rw-r--r--plugins/funind/indfun_common.ml11
-rw-r--r--plugins/funind/indfun_common.mli9
-rw-r--r--proofs/pfedit.ml23
-rw-r--r--proofs/pfedit.mli15
-rw-r--r--test-suite/output/PrintUnivsSubgraph.out5
-rw-r--r--test-suite/output/PrintUnivsSubgraph.v9
-rw-r--r--test-suite/success/Require.v5
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--vernac/g_vernac.mlg8
-rw-r--r--vernac/lemmas.ml23
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/ppvernac.ml5
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/vernacentries.ml48
-rw-r--r--vernac/vernacexpr.ml2
27 files changed, 176 insertions, 178 deletions
diff --git a/CHANGES.md b/CHANGES.md
index e817ac7f36..9ee3c794d7 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -98,6 +98,15 @@ Standard Library
- Added `ByteVector` type that can convert to and from [string].
+- The prelude used to be automatically Exported and is now only
+ Imported. This should be relevant only when importing files which
+ don't use -noinit into files which do.
+
+Universes
+
+- Added `Print Universes Subgraph` variant of `Print Universes`.
+ Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).`
+
Changes from 8.8.2 to 8.9+beta1
===============================
diff --git a/clib/dyn.ml b/clib/dyn.ml
index 6c45767246..22c49706be 100644
--- a/clib/dyn.ml
+++ b/clib/dyn.ml
@@ -38,6 +38,7 @@ sig
type t = Dyn : 'a tag * 'a -> t
val create : string -> 'a tag
+ val anonymous : int -> 'a tag
val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
val repr : 'a tag -> string
@@ -81,15 +82,22 @@ module Self : PreS = struct
let create (s : string) =
let hash = Hashtbl.hash s in
- let () =
- if Int.Map.mem hash !dyntab then
- let old = Int.Map.find hash !dyntab in
- let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
- assert false
- in
- let () = dyntab := Int.Map.add hash s !dyntab in
+ if Int.Map.mem hash !dyntab then begin
+ let old = Int.Map.find hash !dyntab in
+ Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old;
+ assert false
+ end;
+ dyntab := Int.Map.add hash s !dyntab;
hash
+ let anonymous n =
+ if Int.Map.mem n !dyntab then begin
+ Printf.eprintf "Dynamic tag collision: %d\n%!" n;
+ assert false
+ end;
+ dyntab := Int.Map.add n "<anonymous>" !dyntab;
+ n
+
let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
diff --git a/clib/dyn.mli b/clib/dyn.mli
index ff9762bd6b..1bd78b2db8 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -48,6 +48,12 @@ sig
Type names are hashed, so [create] may raise even if no type with
the exact same name was registered due to a collision. *)
+ val anonymous : int -> 'a tag
+ (** [anonymous i] returns a tag describing an [i]-th anonymous type.
+ If [anonymous] is not used together with [create], [max_int] anonymous types
+ are available.
+ [anonymous] raises an exception if [i] is already registered. *)
+
val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
(** [eq t1 t2] returns [Some witness] if [t1] is the same as [t2], [None] otherwise. *)
diff --git a/clib/store.ml b/clib/store.ml
index 1469358c9d..79e26908d7 100644
--- a/clib/store.ml
+++ b/clib/store.ml
@@ -20,70 +20,37 @@ module type S =
sig
type t
type 'a field
+ val field : unit -> 'a field
val empty : t
val set : t -> 'a field -> 'a -> t
val get : t -> 'a field -> 'a option
val remove : t -> 'a field -> t
val merge : t -> t -> t
- val field : unit -> 'a field
end
-module Make () : S =
+module Make() : S =
struct
-
- let next =
- let count = ref 0 in fun () ->
- let n = !count in
- incr count;
- n
-
- type t = Obj.t option array
- (** Store are represented as arrays. For small values, which is typicial,
- is slightly quicker than other implementations. *)
-
-type 'a field = int
-
-let allocate len : t = Array.make len None
-
-let empty : t = [||]
-
-let set (s : t) (i : 'a field) (v : 'a) : t =
- let len = Array.length s in
- let nlen = if i < len then len else succ i in
- let () = assert (0 <= i) in
- let ans = allocate nlen in
- Array.blit s 0 ans 0 len;
- Array.unsafe_set ans i (Some (Obj.repr v));
- ans
-
-let get (s : t) (i : 'a field) : 'a option =
- let len = Array.length s in
- if len <= i then None
- else Obj.magic (Array.unsafe_get s i)
-
-let remove (s : t) (i : 'a field) =
- let len = Array.length s in
- let () = assert (0 <= i) in
- let ans = allocate len in
- Array.blit s 0 ans 0 len;
- if i < len then Array.unsafe_set ans i None;
- ans
-
-let merge (s1 : t) (s2 : t) : t =
- let len1 = Array.length s1 in
- let len2 = Array.length s2 in
- let nlen = if len1 < len2 then len2 else len1 in
- let ans = allocate nlen in
- (** Important: No more allocation from here. *)
- Array.blit s2 0 ans 0 len2;
- for i = 0 to pred len1 do
- let v = Array.unsafe_get s1 i in
- match v with
- | None -> ()
- | Some _ -> Array.unsafe_set ans i v
- done;
- ans
-
-let field () = next ()
-
+ module Dyn = Dyn.Make()
+ module Map = Dyn.Map(struct type 'a t = 'a end)
+
+ type t = Map.t
+ type 'a field = 'a Dyn.tag
+
+ let next = ref 0
+ let field () =
+ let f = Dyn.anonymous !next in
+ incr next;
+ f
+
+ let empty =
+ Map.empty
+ let set s f v =
+ Map.add f v s
+ let get s f =
+ try Some (Map.find f s)
+ with Not_found -> None
+ let remove s f =
+ Map.remove f s
+ let merge s1 s2 =
+ Map.fold (fun (Map.Any (f, v)) s -> Map.add f v s) s1 s2
end
diff --git a/clib/store.mli b/clib/store.mli
index 0c2b2e0856..7cdd1d3bed 100644
--- a/clib/store.mli
+++ b/clib/store.mli
@@ -19,6 +19,9 @@ sig
type 'a field
(** Type of field of such stores *)
+ val field : unit -> 'a field
+ (** Create a new field *)
+
val empty : t
(** Empty store *)
@@ -33,11 +36,7 @@ sig
val merge : t -> t -> t
(** [merge s1 s2] adds all the fields of [s1] into [s2]. *)
-
- val field : unit -> 'a field
- (** Create a new field *)
-
end
-module Make () : S
+module Make() : S
(** Create a new store type. *)
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 3ddfc9aec1..391afcb1f7 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2155,6 +2155,12 @@ If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
language, and can be processed by Graphviz tools. The format is
unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
+.. cmdv:: Print Universes Subgraph(@names)
+
+Prints the graph restricted to the requested names (adjusting
+constraints to preserve the implied transitive constraints between
+kept universes).
+
.. _existential-variables:
Existential variables
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 760410894a..1ce0136c1d 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -862,7 +862,6 @@ module type S =
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
external obj : 'a e -> te Gramext.g_entry = "%identity"
- val parse_token : 'a e -> te Stream.t -> 'a
end
type ('self, 'a) ty_symbol
type ('self, 'f, 'r) ty_rule
@@ -930,18 +929,6 @@ module GMake (L : GLexerType) =
Obj.magic (parse_parsable e p : Obj.t)
let parse_token_stream (e : 'a e) ts : 'a =
Obj.magic (e.estart 0 ts : Obj.t)
- let _warned_using_parse_token = ref false
- let parse_token (entry : 'a e) ts : 'a =
- (* commented: too often warned in Coq...
- if not warned_using_parse_token.val then do {
- eprintf "<W> use of Entry.parse_token ";
- eprintf "deprecated since 2017-06-16\n%!";
- eprintf "use Entry.parse_token_stream instead\n%! ";
- warned_using_parse_token.val := True
- }
- else ();
- *)
- parse_token_stream entry ts
let name e = e.ename
let of_parser n (p : te Stream.t -> 'a) : 'a e =
{egram = gram; ename = n; elocal = false;
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 244ab710dc..1c5fcb7bbf 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -36,7 +36,6 @@ module type S =
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
external obj : 'a e -> te Gramext.g_entry = "%identity"
- val parse_token : 'a e -> te Stream.t -> 'a
end
type ('self, 'a) ty_symbol
type ('self, 'f, 'r) ty_rule
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9ff51fca55..9083156745 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -942,34 +942,36 @@ let check_eq_instances g t1 t2 =
(** Pretty-printing *)
+let pr_umap sep pr map =
+ let cmp (u,_) (v,_) = Level.compare u v in
+ Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map))
+
let pr_arc prl = function
| _, Canonical {univ=u; ltle; _} ->
if UMap.is_empty ltle then mt ()
else
prl u ++ str " " ++
v 0
- (pr_sequence (fun (v, strict) ->
+ (pr_umap Pp.spc (fun (v, strict) ->
(if strict then str "< " else str "<= ") ++ prl v)
- (UMap.bindings ltle)) ++
+ ltle) ++
fnl ()
| u, Equiv v ->
prl u ++ str " = " ++ prl v ++ fnl ()
let pr_universes prl g =
- let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in
- prlist (pr_arc prl) graph
+ pr_umap mt (pr_arc prl) g.entries
(* Dumping constraints to a file *)
let dump_universes output g =
let dump_arc u = function
| Canonical {univ=u; ltle; _} ->
- let u_str = Level.to_string u in
UMap.iter (fun v strict ->
let typ = if strict then Lt else Le in
- output typ u_str (Level.to_string v)) ltle;
+ output typ u v) ltle;
| Equiv v ->
- output Eq (Level.to_string u) (Level.to_string v)
+ output Eq u v
in
UMap.iter dump_arc g.entries
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4336a22b8c..a2cc5b3116 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -86,7 +86,7 @@ val check_subtype : AUContext.t check_function
(** {6 Dumping to a file } *)
val dump_universes :
- (constraint_type -> string -> string -> unit) -> t -> unit
+ (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
(** {6 Debugging} *)
val check_universes_invariants : t -> unit
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index eb3e633892..d4aa598fd8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -59,7 +59,7 @@ module type S =
type e 'a = 'y;
value create : string -> e 'a;
value parse : e 'a -> parsable -> 'a;
- value parse_token : e 'a -> Stream.t te -> 'a;
+ value parse_token_stream : e 'a -> Stream.t te -> 'a;
value name : e 'a -> string;
value of_parser : string -> (Stream.t te -> 'a) -> e 'a;
value print : Format.formatter -> e 'a -> unit;
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d1e7d8a5a8..1cf952576d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -320,10 +320,16 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* let dur1 = System.time_difference tim1 tim2 in *)
(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
(* end; *)
- get_proof_clean true, CEphemeron.create hook
- end
-
+ let open Proof_global in
+ let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+ match entries with
+ | [entry] ->
+ discard_current ();
+ (id,(entry,persistence)), CEphemeron.create hook
+ | _ ->
+ CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
+ end
let generate_functional_principle (evd: Evd.evar_map ref)
interactive_proof
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index cd2ea3ef88..b68b34ca35 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -147,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook =
CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
definition_message id
-
-
-let cook_proof _ =
- let (id,(entry,_,strength)) = Pfedit.cook_proof () in
- (id,(entry,strength))
-
-let get_proof_clean do_reduce =
- let result = cook_proof do_reduce in
- Proof_global.discard_current ();
- result
-
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0c8f40c5cf..c9d153d89f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -45,15 +45,6 @@ val jmeq_refl : unit -> EConstr.constr
val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind ->
Lemmas.declaration_hook CEphemeron.key -> unit
-(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
- abort the proof
-*)
-val get_proof_clean : bool ->
- Names.Id.t *
- (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind)
-
-
-
(* [with_full_print f a] applies [f] to [a] in full printing environment.
This function preserves the print settings
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7b55941874..78080fa203 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -35,16 +35,6 @@ let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
| None -> p,(true,[])
| Some tac -> Proof.run_tactic env tac p))
-let cook_this_proof p =
- match p with
- | { Proof_global.id;entries=[constr];persistence;universes } ->
- (id,(constr,universes,persistence))
- | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
-
-let cook_proof () =
- cook_this_proof (fst
- (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
-
exception NoSuchGoal
let _ = CErrors.register_handler begin function
| NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
@@ -155,10 +145,15 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
start_proof id goal_kind evd sign typ terminator;
try
let status = by tac in
- let _,(const,univs,_) = cook_proof () in
- Proof_global.discard_current ();
- let univs = UState.demote_seff_univs const univs in
- const, status, univs
+ let open Proof_global in
+ let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+ match entries with
+ | [entry] ->
+ discard_current ();
+ let univs = UState.demote_seff_univs entry universes in
+ entry, status, univs
+ | _ ->
+ CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
with reraise ->
let reraise = CErrors.push reraise in
Proof_global.discard_current ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 50ce267c81..76be7936b4 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -29,21 +29,6 @@ val start_proof :
Proof_global.proof_terminator -> unit
(** {6 ... } *)
-(** [cook_proof opacity] turns the current proof (assumed completed) into
- a constant with its name, kind and possible hook (see [start_proof]);
- it fails if there is no current proof of if it is not completed;
- it also tells if the guardness condition has to be inferred. *)
-
-val cook_this_proof :
- Proof_global.proof_object ->
- (Id.t *
- (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
-
-val cook_proof : unit ->
- (Id.t *
- (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
-
-(** {6 ... } *)
(** [get_goal_context n] returns the context of the [n]th subgoal of
the current focused proof or raises a [UserError] if there is no
focused proof or if there is no more subgoals *)
diff --git a/test-suite/output/PrintUnivsSubgraph.out b/test-suite/output/PrintUnivsSubgraph.out
new file mode 100644
index 0000000000..c42e15e4e8
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.out
@@ -0,0 +1,5 @@
+Prop < Set
+Set < i
+ < j
+i < j
+
diff --git a/test-suite/output/PrintUnivsSubgraph.v b/test-suite/output/PrintUnivsSubgraph.v
new file mode 100644
index 0000000000..ec9cf44d4f
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.v
@@ -0,0 +1,9 @@
+
+Universes i j k l.
+
+Definition foo : Type@{j} := Type@{i}.
+
+Definition baz : Type@{k} := Type@{l}.
+
+Print Universes Subgraph(i j).
+(* should print [i < j], not [l < k] (and not prelude universes) *)
diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v
index f851d8c7d9..de5987c4f7 100644
--- a/test-suite/success/Require.v
+++ b/test-suite/success/Require.v
@@ -1,3 +1,8 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+
Require Import Coq.Arith.Plus.
Require Coq.Arith.Minus.
Locate Library Coq.Arith.Minus.
+
+(* Check that Init didn't get exported by the import above *)
+Fail Check nat.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e4d9e9ac25..66469ff0b9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -107,7 +107,7 @@ let load_init_vernaculars cur_feeder opts ~state =
(* Startup LoadPath and Modules *)
(******************************************************************************)
(* prelude_data == From Coq Require Export Prelude. *)
-let prelude_data = "Prelude", Some "Coq", Some true
+let prelude_data = "Prelude", Some "Coq", Some false
let require_libs opts =
if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1d0a5ab0a3..960e74827a 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -989,8 +989,9 @@ GRAMMAR EXTEND Gram
| IDENT "Scope"; s = IDENT -> { PrintScope s }
| IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s }
| IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid }
- | IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (false, fopt) }
- | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (true, fopt) }
+ | b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes";
+ g = OPT printunivs_subgraph; fopt = OPT ne_string ->
+ { PrintUniverses (b, g, fopt) }
| IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) }
| IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) }
| IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) }
@@ -1000,6 +1001,9 @@ GRAMMAR EXTEND Gram
| IDENT "Registered" -> { PrintRegistered }
] ]
;
+ printunivs_subgraph:
+ [ [ IDENT "Subgraph"; "("; l = LIST0 reference; ")" -> { l } ] ]
+ ;
class_rawexpr:
[ [ IDENT "Funclass" -> { FunClass }
| IDENT "Sortclass" -> { SortClass }
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a92b94ac0a..4e847a5590 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -306,17 +306,18 @@ let universe_proof_terminator compute_guard hook =
| Admitted (id,k,pe,ctx) ->
admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
- | Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff = match opaque with
- | Transparent -> false, true
- | Opaque -> true, false
- in
- let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in
- let const = {const with const_entry_opaque = is_opaque} in
- let id = match idopt with
- | None -> id
- | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
- save ~export_seff id const univs compute_guard persistence (hook (Some univs))
+ | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
+ let is_opaque, export_seff = match opaque with
+ | Transparent -> false, true
+ | Opaque -> true, false
+ in
+ let const = {const with const_entry_opaque = is_opaque} in
+ let id = match idopt with
+ | None -> id
+ | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
+ save ~export_seff id const universes compute_guard persistence (hook (Some universes))
+ | Proved (opaque,idopt, _ ) ->
+ CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
end
let standard_proof_terminator compute_guard hook =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c2805674e4..746db61cc3 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -844,8 +844,7 @@ let obligation_terminator name num guard hook auto pf =
let term = Lemmas.universe_proof_terminator guard hook in
match pf with
| Admitted _ -> apply_terminator term pf
- | Proved (opq, id, proof) ->
- let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
+ | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
let env = Global.env () in
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
let ty = entry.Entries.const_entry_type in
@@ -904,6 +903,9 @@ let obligation_terminator name num guard hook auto pf =
with e when CErrors.noncritical e ->
let e = CErrors.push e in
pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+ end
+ | Proved (_, _, _ ) ->
+ CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
let obligation_hook prg obl num auto ctx' _ gr =
let obls, rem = prg.prg_obligations in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1c1faca599..f65fae60ee 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -492,12 +492,13 @@ open Pputils
keyword "Print Hint *"
| PrintHintDbName s ->
keyword "Print HintDb" ++ spc () ++ str s
- | PrintUniverses (b, fopt) ->
+ | PrintUniverses (b, g, fopt) ->
let cmd =
if b then "Print Sorted Universes"
else "Print Universes"
in
- keyword cmd ++ pr_opt str fopt
+ let pr_subgraph = prlist_with_sep spc pr_qualid in
+ keyword cmd ++ pr_opt pr_subgraph g ++ pr_opt str fopt
| PrintName (qid,udecl) ->
keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl
| PrintModuleType qid ->
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index b2fa8ec99f..4761e4bbc2 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -42,7 +42,7 @@ module Vernac_ =
let command_entry_ref = ref noedit_mode
let command_entry =
Gram.Entry.of_parser "command_entry"
- (fun strm -> Gram.Entry.parse_token !command_entry_ref strm)
+ (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm)
end
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1152d8b6b..08aee9533f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -319,7 +319,7 @@ let print_registered () =
hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
-let dump_universes_gen g s =
+let dump_universes_gen prl g s =
let output = open_out s in
let output_constraint, close =
if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin
@@ -344,10 +344,12 @@ let dump_universes_gen g s =
| Univ.Lt -> "<"
| Univ.Le -> "<="
| Univ.Eq -> "="
- in Printf.fprintf output "%s %s %s ;\n" left kind right
+ in
+ Printf.fprintf output "%s %s %s ;\n" left kind right
end, (fun () -> close_out output)
end
in
+ let output_constraint k l r = output_constraint k (prl l) (prl r) in
try
UGraph.dump_universes output_constraint g;
close ();
@@ -357,6 +359,36 @@ let dump_universes_gen g s =
close ();
iraise reraise
+let universe_subgraph ?loc g univ =
+ let open Univ in
+ let sigma = Evd.from_env (Global.env()) in
+ let univs_of q =
+ let q = Glob_term.(GType (UNamed q)) in
+ (* this function has a nice error message for not found univs *)
+ LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q)
+ in
+ let univs = List.fold_left (fun univs q -> LSet.union univs (univs_of q)) LSet.empty g in
+ let csts = UGraph.constraints_for ~kept:(LSet.add Level.prop (LSet.add Level.set univs)) univ in
+ let univ = LSet.fold UGraph.add_universe_unconstrained univs UGraph.initial_universes in
+ UGraph.merge_constraints csts univ
+
+let print_universes ?loc ~sort ~subgraph dst =
+ let univ = Global.universes () in
+ let univ = match subgraph with
+ | None -> univ
+ | Some g -> universe_subgraph ?loc g univ
+ in
+ let univ = if sort then UGraph.sort_universes univ else univ in
+ let pr_remaining =
+ if Global.is_joined_environment () then mt ()
+ else str"There may remain asynchronous universe constraints"
+ in
+ let prl = UnivNames.pr_with_global_universes in
+ begin match dst with
+ | None -> UGraph.pr_universes prl univ ++ pr_remaining
+ | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s
+ end
+
(*********************)
(* "Locate" commands *)
@@ -1818,17 +1850,7 @@ let vernac_print ~atts env sigma =
| PrintCoercionPaths (cls,clt) ->
Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
| PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
- | PrintUniverses (b, dst) ->
- let univ = Global.universes () in
- let univ = if b then UGraph.sort_universes univ else univ in
- let pr_remaining =
- if Global.is_joined_environment () then mt ()
- else str"There may remain asynchronous universe constraints"
- in
- begin match dst with
- | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining
- | Some s -> dump_universes_gen univ s
- end
+ | PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
| PrintHintGoal -> Hints.pr_applicable_hint ()
| PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 594e9eca48..180d763946 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -45,7 +45,7 @@ type printable =
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
| PrintCanonicalConversions
- | PrintUniverses of bool * string option
+ | PrintUniverses of bool * qualid list option * string option
| PrintHint of qualid or_by_notation
| PrintHintGoal
| PrintHintDbName of string
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 03:39:40 +0000