aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comDefinition.ml3
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/g_vernac.mlg2
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/metasyntax.ml2
-rw-r--r--vernac/pvernac.ml4
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/topfmt.ml22
-rw-r--r--vernac/topfmt.mli6
-rw-r--r--vernac/vernacextend.ml2
12 files changed, 33 insertions, 18 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index ef28fc2d77..4cdc60216e 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -156,7 +156,7 @@ let do_assumptions kind nl l =
((sigma,env,ienv),((is_coe,idl),t,imps)))
(sigma,env,empty_internalization_env) l
in
- let sigma = solve_remaining_evars all_and_fail_flags env sigma (Evd.from_env env) in
+ let sigma = solve_remaining_evars all_and_fail_flags env sigma in
(* The universe constraints come from the whole telescope. *)
let sigma = Evd.minimize_universes sigma in
let nf_evar c = EConstr.to_constr sigma c in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 472411ac3a..9c80f1d2f5 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -87,8 +87,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let check_definition (ce, evd, _, imps) =
let env = Global.env () in
- let empty_sigma = Evd.from_env env in
- check_evars_are_solved env evd empty_sigma;
+ check_evars_are_solved env evd;
ce
let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a9c499b192..274c99107f 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -239,7 +239,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
end
let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) =
- check_evars_are_solved env evd (Evd.from_env env);
+ check_evars_are_solved env evd;
let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f405c4d5a9..fbfa997555 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -402,7 +402,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
(* Try further to solve evars, and instantiate them *)
- let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in
+ let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
(* Compute renewed arities *)
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3cdf81ced0..e3f6a87541 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -474,7 +474,7 @@ END
{
let only_starredidentrefs =
- Gram.Entry.of_parser "test_only_starredidentrefs"
+ Pcoq.Entry.of_parser "test_only_starredidentrefs"
(fun strm ->
let rec aux n =
match Util.stream_nth n strm with
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index de020926f6..2443c5d12a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -421,7 +421,7 @@ let start_proof_com ?inference_hook kind thms hook =
let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
let flags = all_and_fail_flags in
let hook = inference_hook in
- let evd = solve_remaining_evars ?hook flags env evd Evd.empty in
+ let evd = solve_remaining_evars ?hook flags env evd in
let ids = List.map RelDecl.get_name ctx in
check_name_freshness (pi1 kind) id;
(* XXX: The nf_evar is critical !! *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 2e5e11bb09..5ab877fae2 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -58,7 +58,7 @@ let pr_registered_grammar name =
| None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
| Some entries ->
let pr_one (Pcoq.AnyEntry e) =
- str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++
+ str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
pr_entry e
in
prlist pr_one entries
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 4761e4bbc2..f26e0d0885 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -41,8 +41,8 @@ module Vernac_ =
let command_entry_ref = ref noedit_mode
let command_entry =
- Gram.Entry.of_parser "command_entry"
- (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm)
+ Pcoq.Entry.of_parser "command_entry"
+ (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
end
diff --git a/vernac/record.ml b/vernac/record.ml
index ac84003266..7bdf6a973f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -160,7 +160,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
in
let (sigma, data) = List.fold_left2_map fold sigma records arities in
let sigma =
- Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in
+ Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in
let fold sigma (typ, sort) (_, newfs) =
let _, univ = compute_constructor_level sigma env_ar newfs in
if not def && (Sorts.is_prop sort ||
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index f842ca5ead..4bf76dae51 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -335,6 +335,20 @@ type execution_phase =
| LoadingRcFile
| InteractiveLoop
+let default_phase = ref InteractiveLoop
+
+let in_phase ~phase f x =
+ let op = !default_phase in
+ default_phase := phase;
+ try
+ let res = f x in
+ default_phase := op;
+ res
+ with exn ->
+ let iexn = Backtrace.add_backtrace exn in
+ default_phase := op;
+ Util.iraise iexn
+
let pr_loc loc =
let fname = loc.Loc.fname in
match fname with
@@ -347,8 +361,8 @@ let pr_loc loc =
int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
str":")
-let pr_phase ?loc phase =
- match phase, loc with
+let pr_phase ?loc () =
+ match !default_phase, loc with
| LoadingRcFile, loc ->
(* For when all errors go through feedback:
str "While loading rcfile:" ++
@@ -363,10 +377,10 @@ let pr_phase ?loc phase =
(* Note: interactive messages such as "foo is defined" are not located *)
None
-let print_err_exn phase any =
+let print_err_exn any =
let (e, info) = CErrors.push any in
let loc = Loc.get_loc info in
- let pre_hdr = pr_phase ?loc phase in
+ let pre_hdr = pr_phase ?loc () in
let msg = CErrors.iprint (e, info) ++ fnl () in
std_logger ?pre_hdr Feedback.Error msg
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 73dcb0064b..0ddf474970 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -61,9 +61,11 @@ type execution_phase =
| LoadingRcFile
| InteractiveLoop
+val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b
+
val pr_loc : Loc.t -> Pp.t
-val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option
-val print_err_exn : execution_phase -> exn -> unit
+val pr_phase : ?loc:Loc.t -> unit -> Pp.t option
+val print_err_exn : exn -> unit
(** [with_output_to_file file f x] executes [f x] with logging
redirected to a file [file] *)
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 3a321ecdb4..35f26cab4d 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -190,7 +190,7 @@ let vernac_extend ~command ?classifier ?entry ext =
| None ->
let e = match entry with
| None -> "COMMAND"
- | Some e -> Pcoq.Gram.Entry.name e
+ | Some e -> Pcoq.Entry.name e
in
let msg = Printf.sprintf "\
Vernac entry \"%s\" misses a classifier. \
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 15:54:15 +0000