aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comInductive.ml5
-rw-r--r--vernac/comInductive.mli1
-rw-r--r--vernac/comProgramFixpoint.ml4
-rw-r--r--vernac/explainErr.ml4
-rw-r--r--vernac/g_vernac.mlg7
-rw-r--r--vernac/himsg.ml32
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/ppvernac.ml6
-rw-r--r--vernac/record.ml10
-rw-r--r--vernac/vernacentries.ml63
-rw-r--r--vernac/vernacexpr.ml12
12 files changed, 67 insertions, 83 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 263ebf5f5a..4664df3182 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
if program_mode then
let hook _ _ vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- Impargs.declare_manual_implicits false gr [imps];
+ Impargs.declare_manual_implicits false gr imps;
let pri = intern_info pri in
Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
in
@@ -234,7 +234,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
in
match rest with
| (n, _) :: _ ->
- unbound_method env' k.cl_impl (get_id n)
+ unbound_method env' sigma k.cl_impl (get_id n)
| _ ->
let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 9bbfb8eec6..7fa99b25cb 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -529,7 +529,7 @@ let warn_non_primitive_record =
(hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (IndRef indsp) ++
strbrk" could not be defined as a primitive record")))
-let declare_mutual_inductive_with_eliminations mie pl impls =
+let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
(* spiwack: raises an error if the structure is supposed to be non-recursive,
but isn't *)
begin match mie.mind_entry_finite with
@@ -543,8 +543,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
let (_, kn), prim = declare_mind mie in
let mind = Global.mind_of_delta_kn kn in
- if match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false
- then warn_non_primitive_record (mind,0);
+ if primitive_expected && not prim then warn_non_primitive_record (mind,0);
Declare.declare_univ_binders (IndRef (mind,0)) pl;
List.iteri (fun i (indimpls, constrimpls) ->
let ind = (mind,i) in
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 1d6f652385..224cce67ad 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -43,6 +43,7 @@ type one_inductive_impls =
Impargs.manual_implicits list (* for constrs *)
val declare_mutual_inductive_with_eliminations :
+ ?primitive_expected:bool ->
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index cc9c83bd17..ae77cf12e5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -215,7 +215,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
- Impargs.declare_manual_implicits false gr [impls]
+ Impargs.declare_manual_implicits false gr impls
in
let typ = it_mkProd_or_LetIn top_arity binders in
hook, name, typ
@@ -223,7 +223,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let hook sigma _ _ l gr =
if Impargs.is_implicit_args () || not (List.is_empty impls) then
- Impargs.declare_manual_implicits false gr [impls]
+ Impargs.declare_manual_implicits false gr impls
in hook, recname, typ
in
(* XXX: Capturing sigma here... bad bad *)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 06428b53f2..2bc95dbfcd 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,8 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
| Notation.PrimTokenNotationError(kind,ctx,sigma,te) ->
wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te)
- | Typeclasses_errors.TypeClassError(env, te) ->
- wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+ | Typeclasses_errors.TypeClassError(env, sigma, te) ->
+ wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te)
| Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
| InductiveError e ->
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 42bee25da3..589b15fd41 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,6 +16,7 @@ open Util
open Names
open Glob_term
open Vernacexpr
+open Impargs
open Constrexpr
open Constrexpr_ops
open Extend
@@ -836,11 +837,11 @@ GRAMMAR EXTEND Gram
];
(* Same as [argument_spec_block], but with only implicit status and names *)
more_implicits_block: [
- [ name = name -> { [(name.CAst.v, Vernacexpr.NotImplicit)] }
+ [ name = name -> { [(name.CAst.v, NotImplicit)] }
| "["; items = LIST1 name; "]" ->
- { List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items }
+ { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
| "{"; items = LIST1 name; "}" ->
- { List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items }
+ { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
]
];
strategy_level:
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9dd321be51..2ef2317d86 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -339,6 +339,20 @@ let explain_actual_type env sigma j t reason =
str "while it is expected to have type" ++ brk(1,1) ++ pt ++
ppreason ++ str ".")
+let explain_incorrect_primitive env sigma j exp =
+ let env = make_all_name_different env sigma in
+ let {uj_val=p;uj_type=t} = j in
+ let t = Reductionops.nf_betaiota env sigma t in
+ let exp = Reductionops.nf_betaiota env sigma exp in
+ (* Actually print *)
+ let pe = pr_ne_context_of (str "In environment") env sigma in
+ let (pt, pct) = pr_explicit env sigma exp t in
+ pe ++
+ hov 0 (
+ str "The primitive" ++ brk(1,1) ++ str (CPrimitives.op_or_type_to_string p) ++ spc () ++
+ str "has type" ++ brk(1,1) ++ pct ++ spc () ++
+ str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str ".")
+
let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let randl = jv_nf_betaiotaevar env sigma randl in
let actualtyp = Reductionops.nf_betaiota env sigma actualtyp in
@@ -720,7 +734,9 @@ let explain_type_error env sigma err =
| Generalization (nvar, c) ->
explain_generalization env sigma nvar c
| ActualType (j, pt) ->
- explain_actual_type env sigma j pt None
+ explain_actual_type env sigma j pt None
+ | IncorrectPrimitive (j, t) ->
+ explain_incorrect_primitive env sigma j t
| CantApplyBadType (t, rator, randl) ->
explain_cant_apply_bad_type env sigma t rator randl
| CantApplyNonFunctional (rator, randl) ->
@@ -1039,12 +1055,10 @@ let explain_module_internalization_error = function
(* Typeclass errors *)
-let explain_not_a_class env c =
- let sigma = Evd.from_env env in
- let c = EConstr.to_constr sigma c in
- pr_constr_env env sigma c ++ str" is not a declared type class."
+let explain_not_a_class env sigma c =
+ pr_econstr_env env sigma c ++ str" is not a declared type class."
-let explain_unbound_method env cid { CAst.v = id } =
+let explain_unbound_method env sigma cid { CAst.v = id } =
str "Unbound method name " ++ Id.print (id) ++ spc () ++
str"of class" ++ spc () ++ pr_global cid ++ str "."
@@ -1059,9 +1073,9 @@ let explain_mismatched_contexts env c i j =
fnl () ++ brk (1,1) ++
hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
-let explain_typeclass_error env = function
- | NotAClass c -> explain_not_a_class env c
- | UnboundMethod (cid, id) -> explain_unbound_method env cid id
+let explain_typeclass_error env sigma = function
+ | NotAClass c -> explain_not_a_class env sigma c
+ | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id
(* Refiner errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index f22354cdbf..d0f42ea16b 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -26,7 +26,7 @@ val explain_inductive_error : inductive_error -> Pp.t
val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
-val explain_typeclass_error : env -> typeclass_error -> Pp.t
+val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t
val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index d22e52e960..f705f347a3 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1033,9 +1033,9 @@ open Pputils
let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
let pr_if b x = if b then x else str "" in
let pr_br imp x = match imp with
- | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
- | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
- | Vernacexpr.NotImplicit -> x in
+ | Impargs.Implicit -> str "[" ++ x ++ str "]"
+ | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
+ | Impargs.NotImplicit -> x in
let rec print_arguments n l =
match n, l with
| Some 0, l -> spc () ++ str"/" ++ print_arguments None l
diff --git a/vernac/record.ml b/vernac/record.ml
index 0bd15e203b..3202c9bed2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -416,8 +416,6 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
let primitive =
!primitive_flag &&
List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
- (* will warn_non_primitive_record in declare_projections if we try
- to declare a 0-field record *)
in
let mie =
{ mind_entry_params = params;
@@ -431,7 +429,9 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
in
let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let impls = List.map (fun _ -> paramimpls, []) record_data in
- let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls in
+ let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
+ ~primitive_expected:!primitive_flag
+ in
let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
let rsp = (kn, i) in (* This is ind path of idstruc *)
let cstr = (rsp, 1) in
@@ -487,8 +487,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
(DefinitionEntry proj_entry, IsDefinition Definition)
in
let cref = ConstRef cst in
- Impargs.declare_manual_implicits false cref [paramimpls];
- Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+ Impargs.declare_manual_implicits false cref paramimpls;
+ Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d9d824ad98..d227834fcf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -16,7 +16,6 @@ open CAst
open Util
open Names
open Nameops
-open Term
open Tacmach
open Constrintern
open Prettyp
@@ -32,6 +31,7 @@ open Lemmas
open Locality
open Attributes
+module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(** TODO: make this function independent of Ltac *)
@@ -133,22 +133,23 @@ let show_intro all =
*)
let make_cases_aux glob_ref =
+ let open Declarations in
match glob_ref with
| Globnames.IndRef ind ->
- let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+ let mib, mip = Global.lookup_inductive ind in
Util.Array.fold_right_i
- (fun i typ l ->
- let al = List.rev (fst (decompose_prod typ)) in
- let al = Util.List.skipn np al in
+ (fun i (ctx, _) l ->
+ let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
let rec rename avoid = function
| [] -> []
- | (n,_)::l ->
+ | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
+ | RelDecl.LocalAssum (n, _)::l ->
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
Id.to_string n' :: rename (Id.Set.add n' avoid) l in
let al' = rename Id.Set.empty al in
let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
- tarr []
+ mip.mind_nf_lc []
| _ -> raise Not_found
let make_cases s =
@@ -1173,14 +1174,6 @@ let vernac_syntactic_definition ~module_local lid x y =
Dumpglob.dump_definition lid false "syndef";
Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
-let vernac_declare_implicits ~section_local r l =
- match l with
- | [] ->
- Impargs.declare_implicits section_local (smart_global r)
- | _::_ as imps ->
- Impargs.declare_manual_implicits section_local (smart_global r) ~enriching:false
- (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
-
let warn_arguments_assert =
CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
(fun sr ->
@@ -1336,43 +1329,15 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
end;
- (* Parts of this code are overly complicated because the implicit arguments
- API is completely crazy: positions (ExplByPos) are elaborated to
- names. This is broken by design, since not all arguments have names. So
- even though we eventually want to map only positions to implicit statuses,
- we have to check whether the corresponding arguments have names, not to
- trigger an error in the impargs code. Even better, the names we have to
- check are not the current ones (after previous renamings), but the original
- ones (inferred from the type). *)
-
let implicits =
List.map (fun { name; implicit_status = i } -> (name,i)) args
in
let implicits = implicits :: more_implicits in
- let open Vernacexpr in
- let rec build_implicits inf_names implicits =
- match inf_names, implicits with
- | _, [] -> []
- | _ :: inf_names, (_, NotImplicit) :: implicits ->
- build_implicits inf_names implicits
-
- (* With the current impargs API, it is impossible to make an originally
- anonymous argument implicit *)
- | Anonymous :: _, (name, _) :: _ ->
- user_err ~hdr:"vernac_declare_arguments"
- (strbrk"Argument "++ Name.print name ++
- strbrk " cannot be declared implicit.")
-
- | Name id :: inf_names, (name, impl) :: implicits ->
- let max = impl = MaximallyImplicit in
- (ExplByName id,max,false) :: build_implicits inf_names implicits
-
- | _ -> assert false (* already checked in [names_union] *)
- in
-
- let implicits = List.map (build_implicits inf_names) implicits in
- let implicits_specified = match implicits with [[]] -> false | _ -> true in
+ let implicits = List.map (List.map snd) implicits in
+ let implicits_specified = match implicits with
+ | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+ | _ -> true in
if implicits_specified && clear_implicits_flag then
user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
@@ -1415,10 +1380,10 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
end;
if implicits_specified || clear_implicits_flag then
- vernac_declare_implicits ~section_local reference implicits;
+ Impargs.set_implicits section_local (smart_global reference) implicits;
if default_implicits_flag then
- vernac_declare_implicits ~section_local reference [];
+ Impargs.declare_implicits section_local (smart_global reference);
if red_modifiers_specified then begin
match sr with
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2eb901890b..d1da7c0602 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -237,13 +237,11 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative
(** {6 The type of vernacular expressions} *)
-type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
type vernac_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
- implicit_status : vernac_implicit_status;
+ implicit_status : Impargs.implicit_kind;
}
type extend_name =
@@ -355,7 +353,7 @@ type nonrec vernac_expr =
onlyparsing_flag
| VernacArguments of qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
- (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
+ (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
int option (* Number of args to trigger reduction *) *
[ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
`ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
@@ -409,3 +407,9 @@ type vernac_control =
| VernacRedirect of string * vernac_control CAst.t
| VernacTimeout of int * vernac_control
| VernacFail of vernac_control
+
+(** Deprecated *)
+
+type vernac_implicit_status = Impargs.implicit_kind =
+ | Implicit [@ocaml.deprecated] | MaximallyImplicit [@ocaml.deprecated] | NotImplicit [@ocaml.deprecated]
+[@@ocaml.deprecated "Use [Impargs.implicit_kind]"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 18:33:26 +0000