aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/comInductive.ml20
-rw-r--r--vernac/comInductive.mli5
-rw-r--r--vernac/explainErr.ml1
-rw-r--r--vernac/himsg.ml31
-rw-r--r--vernac/himsg.mli1
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/metasyntax.ml11
-rw-r--r--vernac/mltop.ml2
-rw-r--r--vernac/ppvernac.ml6
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/record.ml4
-rw-r--r--vernac/topfmt.ml21
-rw-r--r--vernac/topfmt.mli1
-rw-r--r--vernac/vernacentries.ml26
-rw-r--r--vernac/vernacstate.ml12
-rw-r--r--vernac/vernacstate.mli4
17 files changed, 103 insertions, 52 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 370df615fc..a342f5bf98 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -301,10 +301,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
else tclass
in
- let sigma, k, u, cty, ctx', ctx, len, imps, subst =
+ let sigma, k, u, cty, ctx', ctx, imps, subst =
let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
- let len = List.length ctx in
+ let len = Context.Rel.nhyps ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum sigma c' in
let ctx'' = ctx' @ ctx in
@@ -320,7 +320,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
| LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
cl_context (args, [])
in
- sigma, cl, u, c', ctx', ctx, len, imps, args
+ sigma, cl, u, c', ctx', ctx, imps, args
in
let id =
match instid with
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 4af6415a4d..92b1ff7572 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -24,7 +24,7 @@ open Constrexpr_ops
open Constrintern
open Impargs
open Reductionops
-open Indtypes
+open Type_errors
open Pretyping
open Indschemes
open Context.Rel.Declaration
@@ -34,6 +34,13 @@ module RelDecl = Context.Rel.Declaration
(* 3b| Mutual inductive definitions *)
+let warn_auto_template =
+ CWarnings.create ~name:"auto-template" ~category:"vernacular" ~default:CWarnings.Disabled
+ (fun id ->
+ Pp.(strbrk "Automatically declaring " ++ Id.print id ++
+ strbrk " as template polymorphic. Use attributes or " ++
+ strbrk "disable Auto Template Polymorphism to avoid this warning."))
+
let should_auto_template =
let open Goptions in
let auto = ref true in
@@ -44,7 +51,10 @@ let should_auto_template =
optread = (fun () -> !auto);
optwrite = (fun b -> auto := b); }
in
- fun () -> !auto
+ fun id would_auto ->
+ let b = !auto && would_auto in
+ if b then warn_auto_template id;
+ b
let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
| CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
@@ -294,7 +304,7 @@ let inductive_levels env evd poly arities inds =
let evd =
if Sorts.is_set du then
if not (Evd.check_leq evd cu Univ.type0_univ) then
- raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
+ raise (InductiveError LargeNonPropInductiveNotInType)
else evd
else evd
(* Evd.set_leq_sort env evd (Type cu) du *)
@@ -431,8 +441,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
template
| None ->
- should_auto_template () && not poly &&
- Option.cata (fun s -> not (Sorts.is_small s)) false concl
+ should_auto_template ind.ind_name (not poly &&
+ Option.cata (fun s -> not (Sorts.is_small s)) false concl)
in
{ mind_entry_typename = ind.ind_name;
mind_entry_arity = arity;
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 9df8f7c341..1d6f652385 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -46,7 +46,10 @@ val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
-val should_auto_template : unit -> bool
+val should_auto_template : Id.t -> bool -> bool
+(** [should_auto_template x b] is [true] when [b] is [true] and we
+ automatically use template polymorphism. [x] is the name of the
+ inductive under consideration. *)
(** Exported for Funind *)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index e1496e58d7..71770a21ca 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -10,7 +10,6 @@
open Pp
open CErrors
-open Indtypes
open Type_errors
open Pretype_errors
open Indrec
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a2b5c8d70a..ebbec86b9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -15,7 +15,6 @@ open Nameops
open Namegen
open Constr
open Termops
-open Indtypes
open Environ
open Pretype_errors
open Type_errors
@@ -511,7 +510,7 @@ let pr_trailing_ne_context_of env sigma =
if List.is_empty (Environ.rel_context env) &&
List.is_empty (Environ.named_context env)
then str "."
- else (str " in environment:"++ pr_context_unlimited env sigma)
+ else (strbrk " in environment:" ++ pr_context_unlimited env sigma)
let rec explain_evar_kind env sigma evk ty =
let open Evar_kinds in
@@ -551,21 +550,21 @@ let rec explain_evar_kind env sigma evk ty =
strbrk "an instance of type " ++ ty ++
str " for the variable " ++ Id.print id
| Evar_kinds.SubEvar (where,evk') ->
- let evi = Evd.find sigma evk' in
+ let rec find_source evk =
+ let evi = Evd.find sigma evk in
+ match snd evi.evar_source with
+ | Evar_kinds.SubEvar (_,evk) -> find_source evk
+ | src -> evi,src in
+ let evi,src = find_source evk' in
let pc = match evi.evar_body with
| Evar_defined c -> pr_leconstr_env env sigma c
| Evar_empty -> assert false in
let ty' = evi.evar_concl in
- (match where with
- | Some Evar_kinds.Body -> str "the body of "
- | Some Evar_kinds.Domain -> str "the domain of "
- | Some Evar_kinds.Codomain -> str "the codomain of "
- | None ->
- pr_existential_key sigma evk ++ str " of type " ++ ty ++
- str " in the partial instance " ++ pc ++
- str " found for ") ++
- explain_evar_kind env sigma evk'
- (pr_leconstr_env env sigma ty') (snd evi.evar_source)
+ pr_existential_key sigma evk ++
+ strbrk " in the partial instance " ++ pc ++
+ strbrk " found for " ++
+ explain_evar_kind env sigma evk
+ (pr_leconstr_env env sigma ty') src
let explain_typeclass_resolution env sigma evi k =
match Typeclasses.class_of_constr sigma evi.evar_concl with
@@ -1163,6 +1162,9 @@ let error_bad_entry () =
let error_large_non_prop_inductive_not_in_type () =
str "Large non-propositional inductive types must be in Type."
+let error_inductive_bad_univs () =
+ str "Incorrect universe constrains declared for inductive type."
+
(* Recursion schemes errors *)
let error_not_allowed_case_analysis env isrec kind i =
@@ -1199,7 +1201,8 @@ let explain_inductive_error = function
| NotAnArity (env, c) -> error_not_an_arity env c
| BadEntry -> error_bad_entry ()
| LargeNonPropInductiveNotInType ->
- error_large_non_prop_inductive_not_in_type ()
+ error_large_non_prop_inductive_not_in_type ()
+ | BadUnivs -> error_inductive_bad_univs ()
(* Recursion schemes errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index bab66b2af4..986906d303 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Indtypes
open Environ
open Type_errors
open Pretype_errors
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1a6eda446c..8f155adb8a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -483,7 +483,7 @@ let save_proof ?proof = function
let pftree = Proof_global.give_me_the_proof () in
let id, k, typ = Pfedit.current_proof_statement () in
let typ = EConstr.Unsafe.to_constr typ in
- let universes = Proof.initial_euctx pftree in
+ let universes = Proof.((data pftree).initial_euctx) in
(* This will warn if the proof is complete *)
let pproofs, _univs =
Proof_global.return_proof ~allow_partial:true () in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 790b62c9d0..3da12e7714 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1359,7 +1359,7 @@ let inNotation : notation_obj -> obj =
(**********************************************************************)
let with_lib_stk_protection f x =
- let fs = Lib.freeze ~marshallable:`No in
+ let fs = Lib.freeze ~marshallable:false in
try let a = f x in Lib.unfreeze fs; a
with reraise ->
let reraise = CErrors.push reraise in
@@ -1563,14 +1563,17 @@ let add_notation_extra_printing_rule df k v =
(* Infix notations *)
-let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None)
let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
- let metas = [inject_var "x"; inject_var "y"] in
+ let vars = names_of_constr_expr pr in
+ let x = Namegen.next_ident_away (Id.of_string "x") vars in
+ let y = Namegen.next_ident_away (Id.of_string "y") vars in
+ let metas = [inject_var x; inject_var y] in
let c = mkAppC (pr,metas) in
- let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in
+ let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
add_notation local env c (df,modifiers) sc
(**********************************************************************)
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 3620e177fe..8d6268753e 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -394,7 +394,7 @@ let unfreeze_ml_modules x =
let _ =
Summary.declare_ml_modules_summary
- { Summary.freeze_function = (fun _ -> get_loaded_modules ());
+ { Summary.freeze_function = (fun ~marshallable -> get_loaded_modules ());
Summary.unfreeze_function = unfreeze_ml_modules;
Summary.init_function = reset_loaded_modules }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 8535585749..e0dd3380f9 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -700,7 +700,7 @@ open Pputils
| None -> mt()
| Some r ->
keyword "Eval" ++ spc() ++
- pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
+ Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
keyword " in" ++ spc()
in
let pr_def_body = function
@@ -1134,7 +1134,7 @@ open Pputils
let pr_mayeval r c = match r with
| Some r0 ->
hov 2 (keyword "Eval" ++ spc() ++
- pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
+ Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
| None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
in
@@ -1146,7 +1146,7 @@ open Pputils
| VernacDeclareReduction (s,r) ->
return (
keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
- pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
+ Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
)
| VernacPrint p ->
return (pr_printable p)
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index f26e0d0885..a647b2ef73 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,4 +52,4 @@ let set_command_entry e = Vernac_.command_entry_ref := e
let get_command_entry () = !Vernac_.command_entry_ref
let () =
- register_grammar Stdarg.wit_red_expr (Vernac_.red_expr);
+ register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/record.ml b/vernac/record.ml
index ffd4f654c6..2867ad1437 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -415,9 +415,9 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
template
| None, template ->
(* auto detect template *)
- ComInductive.should_auto_template () && template && not poly &&
+ ComInductive.should_auto_template id (template && not poly &&
let _, s = Reduction.dest_arity (Global.env()) arity in
- not (Sorts.is_small s)
+ not (Sorts.is_small s))
in
{ mind_entry_typename = id;
mind_entry_arity = arity;
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 4065bb9c1f..b4b893a3fd 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -406,3 +406,24 @@ let with_output_to_file fname func input =
deep_ft := Util.pi3 old_fmt;
close_out channel;
Exninfo.iraise reraise
+
+(* For coqtop -time, we display the position in the file,
+ and a glimpse of the executed command *)
+
+let pr_cmd_header {CAst.loc;v=com} =
+ let shorten s =
+ if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+ in
+ let noblank s = String.map (fun c ->
+ match c with
+ | ' ' | '\n' | '\t' | '\r' -> '~'
+ | x -> x
+ ) s
+ in
+ let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+ let safe_pr_vernac x =
+ try Ppvernac.pr_vernac x
+ with e -> str (Printexc.to_string e) in
+ let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
+ in str "Chars " ++ int start ++ str " - " ++ int stop ++
+ str " [" ++ str cmd ++ str "] "
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 0ddf474970..5f84c5edee 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -71,3 +71,4 @@ val print_err_exn : exn -> unit
redirected to a file [file] *)
val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c6c6f74152..dbccea1117 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -82,12 +82,12 @@ let show_proof () =
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
let pfts = Proof_global.give_me_the_proof () in
- let gls,_,shelf,givenup,sigma = Proof.proof pfts in
- pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma)
+ let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in
+ pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
let show_universes () =
let pfts = Proof_global.give_me_the_proof () in
- let gls,_,_,_,sigma = Proof.proof pfts in
+ let Proof.{goals;sigma} = Proof.data pfts in
let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++
str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx
@@ -96,9 +96,9 @@ let show_universes () =
let show_intro all =
let open EConstr in
let pf = Proof_global.give_me_the_proof() in
- let gls,_,_,_,sigma = Proof.proof pf in
- if not (List.is_empty gls) then begin
- let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
+ let Proof.{goals;sigma} = Proof.data pf in
+ if not (List.is_empty goals) then begin
+ let gl = {Evd.it=List.hd goals ; sigma = sigma; } in
let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
if all then
let lid = Tactics.find_intro_names l gl in
@@ -1047,8 +1047,9 @@ let vernac_set_end_tac tac =
let vernac_set_used_variables e =
let env = Global.env () in
+ let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
let tys =
- List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
+ List.map snd (initial_goals (Proof_global.give_me_the_proof ())) in
let tys = List.map EConstr.Unsafe.to_constr tys in
let l = Proof_using.process_expr env e tys in
let vars = Environ.named_context env in
@@ -1815,8 +1816,8 @@ let vernac_global_check c =
let get_nth_goal n =
let pf = Proof_global.give_me_the_proof() in
- let gls,_,_,_,sigma = Proof.proof pf in
- let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
+ let Proof.{goals;sigma} = Proof.data pf in
+ let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
gl
exception NoHyp
@@ -2387,8 +2388,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
control v
| VernacRedirect (s, {v}) ->
Topfmt.with_output_to_file s control v
- | VernacTime (batch, {v}) ->
- System.with_time ~batch control v;
+ | VernacTime (batch, com) ->
+ let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in
+ System.with_time ~batch ~header control com.CAst.v;
and aux ~atts : _ -> unit =
function
@@ -2435,7 +2437,7 @@ let interp ?verbosely ?proof ~st cmd =
Vernacstate.unfreeze_interp_state st;
try
interp ?verbosely ?proof ~st cmd;
- Vernacstate.freeze_interp_state `No
+ Vernacstate.freeze_interp_state ~marshallable:false
with exn ->
let exn = CErrors.push exn in
Vernacstate.invalidate_cache ();
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index aa8bcdc328..61540024ef 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -33,11 +33,19 @@ let do_if_not_cached rf f v =
| Some _ ->
()
-let freeze_interp_state marshallable =
+let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
proof = update_cache s_proof (Proof_global.freeze ~marshallable);
- shallow = marshallable = `Shallow }
+ shallow = false;
+ }
let unfreeze_interp_state { system; proof } =
do_if_not_cached s_cache States.unfreeze system;
do_if_not_cached s_proof Proof_global.unfreeze proof
+
+let make_shallow st =
+ let lib = States.lib_of_state st.system in
+ { st with
+ system = States.replace_lib st.system @@ Lib.drop_objects lib;
+ shallow = true;
+ }
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b4d478d12d..ed20cb935a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -14,8 +14,10 @@ type t = {
shallow : bool (* is the state trimmed down (libstack) *)
}
-val freeze_interp_state : Summary.marshallable -> t
+val freeze_interp_state : marshallable:bool -> t
val unfreeze_interp_state : t -> unit
+val make_shallow : t -> t
+
(* WARNING: Do not use, it will go away in future releases *)
val invalidate_cache : unit -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 22:00:53 +0000