aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml4
-rw-r--r--interp/constrexpr_ops.ml4
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrintern.ml14
-rw-r--r--interp/declare.mli2
-rw-r--r--interp/impargs.ml4
-rw-r--r--interp/impargs.mli6
-rw-r--r--interp/implicit_quantifiers.ml59
-rw-r--r--interp/syntax_def.ml2
9 files changed, 48 insertions, 49 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 9f778d99e9..3ebbbdfb88 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -40,8 +40,8 @@ type explicitation =
type binder_kind =
| Default of binding_kind
- | Generalized of binding_kind * binding_kind * bool
- (** Inner binding, outer bindings, typeclass-specific flag
+ | Generalized of binding_kind * bool
+ (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
type abstraction_kind = AbsLambda | AbsPi
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 443473d5b6..bcb2f34377 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -34,8 +34,8 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
let binder_kind_eq b1 b2 = match b1, b2 with
| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
-| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
- binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+| Generalized (ck1, b1), Generalized (ck2, b2) ->
+ binding_kind_eq ck1 ck2 &&
(if b1 then b2 else not b2)
| _ -> false
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bb66658a37..fe50bd4b08 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -107,7 +107,7 @@ let _show_inactive_notations () =
let deactivate_notation nr =
match nr with
| SynDefRule kn ->
- (* shouldn't we check wether it is well defined? *)
+ (* shouldn't we check whether it is well defined? *)
inactive_notations_table := IRuleSet.add nr !inactive_notations_table
| NotationRule (scopt, ntn) ->
match availability_of_notation (scopt, ntn) (scopt, []) with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f06493b374..31f3736bae 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -389,7 +389,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
{env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
let intern_generalized_binder ?(global_level=false) intern_type ntnvars
- env {loc;v=na} b b' t ty =
+ env {loc;v=na} b' t ty =
let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
let ty, ids' =
if t then ty, ids else
@@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
env fvs in
let bl = List.map
CAst.(map (fun id ->
- (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+ (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -433,8 +433,8 @@ let intern_assumption intern ntnvars env nal bk ty =
(push_name_env ntnvars impls env locna,
(make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
- | Generalized (b,b',t) ->
- let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in
+ | Generalized (b',t) ->
+ let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in
env, b
let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
@@ -1229,7 +1229,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with
let maxargs = Inductiveops.constructor_nalldecls env cstr in
if List.length pl' + List.length args > maxargs then
error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
- (* Two possibilities: either the args are given with explict
+ (* Two possibilities: either the args are given with explicit
variables for local definitions, then we give the explicit args
extended with local defs, so that there is nothing more to be
added later on; or the args are not enough to have all arguments,
@@ -1467,7 +1467,7 @@ let alias_of als = match als.alias_ids with
@returns a raw_case_pattern_expr :
- no notations and syntactic definition
- - global reference and identifeir instead of reference
+ - global reference and identifier instead of reference
*)
@@ -1642,7 +1642,7 @@ let drop_notations_pattern looked_for genv =
| CPatCast (_,_) ->
(* We raise an error if the pattern contains a cast, due to
current restrictions on casts in patterns. Cast in patterns
- are supportted only in local binders and only at top
+ are supported only in local binders and only at top
level. In fact, they are currently eliminated by the
parser. The only reason why they are in the
[cases_pattern_expr] type is that the parser needs to factor
diff --git a/interp/declare.mli b/interp/declare.mli
index 2ffde31fc0..795d9a767d 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -40,7 +40,7 @@ type internal_flag =
| InternalTacticRequest
| UserIndividualRequest
-(* Defaut definition entries, transparent with no secctx or proj information *)
+(* Default definition entries, transparent with no secctx or proj information *)
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:types ->
?univs:Entries.universes_entry ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 806fe93297..f3cdd64633 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -96,11 +96,11 @@ let set_maximality imps b =
this kind if there is enough arguments to infer them)
- [DepFlex] means that the implicit argument can be found by unification
- along a collapsable path only (e.g. as x in (P x) where P is another
+ along a collapsible path only (e.g. as x in (P x) where P is another
argument) (we do (defensively) print the arguments of this kind)
- [DepFlexAndRigid] means that the least argument from which the
- implicit argument can be inferred is following a collapsable path
+ implicit argument can be inferred is following a collapsible path
but there is a greater argument from where the implicit argument is
inferable following a rigid path (useful to know how to print a
partial application)
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ccdd448460..1099074c63 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
(** {6 ... } *)
(** An [implicits_list] is a list of positions telling which arguments
- of a reference can be automatically infered *)
+ of a reference can be automatically inferred *)
type argument_position =
@@ -50,11 +50,11 @@ type implicit_explanation =
this kind if there is enough arguments to infer them) *)
| DepFlex of argument_position
(** means that the implicit argument can be found by unification
- along a collapsable path only (e.g. as x in (P x) where P is another
+ along a collapsible path only (e.g. as x in (P x) where P is another
argument) (we do (defensively) print the arguments of this kind) *)
| DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
(** means that the least argument from which the
- implicit argument can be inferred is following a collapsable path
+ implicit argument can be inferred is following a collapsible path
but there is a greater argument from where the implicit argument is
inferable following a rigid path (useful to know how to print a
partial application) *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 6277d874dd..bac46c2d2f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -196,10 +196,9 @@ let combine_params avoid fn applied needed =
user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
-let combine_params_freevar =
- fun avoid (_, decl) ->
- let id' = next_name_away_from (RelDecl.get_name decl) avoid in
- (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
+let combine_params_freevar avoid (_, decl) =
+ let id' = next_name_away_from (RelDecl.get_name decl) avoid in
+ (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
let destClassApp cl =
let open CAst in
@@ -222,34 +221,34 @@ let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
- let gr = Nametab.locate qid in
- if Typeclasses.is_class gr then Some (clapp, gr) else None
+ if Libnames.idset_mem_qualid qid env then None
+ else
+ let gr = Nametab.locate qid in
+ if Typeclasses.is_class gr then Some (clapp, gr) else None
with Not_found -> None
in
- match is_class with
- | None -> ty, env
- | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
- let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
- let c, avoid =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let c = class_info env sigma gr in
- let (ci, rd) = c.cl_context in
- if not allow_partial then
- begin
- let opt_succ x n = match x with
- | None -> succ n
- | Some _ -> n
- in
- let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
- let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
- if not (Int.equal needlen applen) then
- mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
- end;
- let pars = List.rev (List.combine ci rd) in
- let args, avoid = combine_params avoid f par pars in
- CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
- in c, avoid
+ match is_class with
+ | None -> ty, env
+ | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
+ let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let c = class_info env sigma gr in
+ let (ci, rd) = c.cl_context in
+ if not allow_partial then
+ begin
+ let opt_succ x n = match x with
+ | None -> succ n
+ | Some _ -> n
+ in
+ let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+ let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+ if not (Int.equal needlen applen) then
+ mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+ end;
+ let pars = List.rev (List.combine ci rd) in
+ let args, avoid = combine_params avoid f par pars in
+ CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
let warn_ignoring_implicit_status =
CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 49273c4146..a7e1de736c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
match onlyparse with
| None ->
(* Redeclare it to be used as (short) name in case an other (distfix)
- notation was declared inbetween *)
+ notation was declared in between *)
Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
| _ -> ()
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:20:35 +0000