aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/himsg.ml14
-rw-r--r--vernac/indschemes.ml18
-rw-r--r--vernac/prettyp.ml6
5 files changed, 24 insertions, 20 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 310ea62a1d..f954915cf8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -430,7 +430,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
end
(* used in the bool -> leb side *)
-let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let open EConstr in
let avoid = Array.of_list aavoid in
let do_arg sigma hd v offset =
@@ -658,7 +658,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
then
Tacticals.New.tclTHEN
- (do_replace_bl mode bl_scheme_key ind
+ (do_replace_bl bl_scheme_key ind
(!avoid)
nparrec (ca.(2))
(ca.(1)))
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0e17f2b274..d48e2139d1 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -200,7 +200,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
Constrintern.Recursive full_arity impls
in
let newimpls = Id.Map.singleton recname
- (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+ (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
scopes @ [None]) in
interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
~impls:newimpls body (lift 1 top_arity)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2e58bf4a93..19ec0a3642 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -117,8 +117,8 @@ let display_eq ~flags env sigma t1 t2 =
let open Constrextern in
let t1 = canonize_constr sigma t1 in
let t2 = canonize_constr sigma t2 in
- let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in
- let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in
+ let ct1 = Flags.with_options flags (fun () -> extern_constr env sigma t1) () in
+ let ct2 = Flags.with_options flags (fun () -> extern_constr env sigma t2) () in
Constrexpr_ops.constr_expr_eq ct1 ct2
(** This function adds some explicit printing flags if the two arguments are
@@ -134,9 +134,9 @@ let rec pr_explicit_aux env sigma t1 t2 = function
pr_explicit_aux env sigma t1 t2 rem
else
let open Constrextern in
- let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) ()
+ let ct1 = Flags.with_options flags (fun () -> extern_constr env sigma t1) ()
in
- let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
+ let ct2 = Flags.with_options flags (fun () -> extern_constr env sigma t2) ()
in
Ppconstr.pr_lconstr_expr env sigma ct1, Ppconstr.pr_lconstr_expr env sigma ct2
@@ -697,7 +697,7 @@ let explain_cannot_find_well_typed_abstraction env sigma p l e =
str "Abstracting over the " ++
str (String.plural (List.length l) "term") ++ spc () ++
hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++
- str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env sigma p ++
+ str "leads to a term" ++ spc () ++ pr_ltype_env ~goal_concl_style:true env sigma p ++
spc () ++ str "which is ill-typed." ++
(match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
@@ -1183,7 +1183,7 @@ let error_ill_formed_constructor env id c v nparams nargs =
let pr_ltype_using_barendregt_convention_env env c =
(* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
- quote (pr_goal_concl_style_env env (Evd.from_env env) (EConstr.of_constr c))
+ quote (pr_ltype_env ~goal_concl_style:true env (Evd.from_env env) c)
let error_bad_ind_parameters env c n v1 v2 =
let pc = pr_ltype_using_barendregt_convention_env env c in
@@ -1338,7 +1338,7 @@ let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
let e = map_ptype_error EConstr.of_constr e in
str "The abstracted term" ++ spc () ++
- quote (pr_goal_concl_style_env env sigma c) ++
+ quote (pr_letype_env ~goal_concl_style:true env sigma c) ++
spc () ++ str "is not well typed." ++ fnl () ++
explain_type_error env' (Evd.from_env env') e
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b2e1a5e796..2f0b1062a7 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -210,7 +210,7 @@ let declare_one_case_analysis_scheme ind =
induction scheme, the other ones share the same code with the
appropriate type *)
if Sorts.family_leq InType kelim then
- ignore (define_individual_scheme dep UserAutomaticRequest None ind)
+ define_individual_scheme dep UserAutomaticRequest None ind
(* Induction/recursion schemes *)
@@ -248,7 +248,7 @@ let declare_one_induction_scheme ind =
else if depelim then kinds_from_type
else nondep_kinds_from_type)
in
- List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
+ List.iter (fun kind -> define_individual_scheme kind UserAutomaticRequest None ind)
elims
let declare_induction_schemes kn =
@@ -264,7 +264,7 @@ let declare_induction_schemes kn =
let declare_eq_decidability_gen internal names kn =
let mib = Global.lookup_mind kn in
if mib.mind_finite <> Declarations.CoFinite then
- ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
+ define_mutual_scheme eq_dec_scheme_kind internal names kn
let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind)
@@ -280,14 +280,14 @@ let try_declare_eq_decidability kn =
let declare_eq_decidability = declare_eq_decidability_scheme_with []
let ignore_error f x =
- try ignore (f x) with e when CErrors.noncritical e -> ()
+ try f x with e when CErrors.noncritical e -> ()
let declare_rewriting_schemes ind =
if Hipattern.is_inductive_equality ind then begin
- ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
- ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
- ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
- UserAutomaticRequest None ind);
+ define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind;
+ define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind;
+ define_individual_scheme rew_r2l_forward_dep_scheme_kind
+ UserAutomaticRequest None ind;
(* These ones expect the equality to be symmetric; the first one also *)
(* needs eq *)
ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
@@ -310,7 +310,7 @@ let declare_congr_scheme ind =
try Coqlib.check_required_library Coqlib.logic_module_name; true
with e when CErrors.noncritical e -> false
then
- ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
+ define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind
else
warn_cannot_build_congruence ()
end
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ea49cae9db..eb7b28f15b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -255,9 +255,13 @@ let needs_extra_scopes ref scopes =
let ty, _ctx = Typeops.type_of_global_in_context env ref in
aux env ty scopes
+let implicit_name_of_pos = function
+ | Constrexpr.ExplByName id -> Name id
+ | Constrexpr.ExplByPos (n,k) -> Anonymous
+
let implicit_kind_of_status = function
| None -> Anonymous, NotImplicit
- | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
+ | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
let dummy = {
Vernacexpr.implicit_status = NotImplicit;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 18:00:23 +0000