aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml10
-rw-r--r--interp/constrintern.ml61
-rw-r--r--interp/constrintern.mli7
-rw-r--r--interp/declare.ml16
-rw-r--r--interp/declare.mli5
-rw-r--r--interp/discharge.ml17
-rw-r--r--interp/genintern.ml15
-rw-r--r--interp/genintern.mli9
-rw-r--r--interp/impargs.ml6
-rw-r--r--interp/interp.mllib2
-rw-r--r--interp/modintern.ml64
-rw-r--r--interp/notation.ml6
-rw-r--r--interp/notation_ops.ml4
13 files changed, 167 insertions, 55 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 601099c6ff..838ef40545 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -480,6 +480,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(make_pat_notation ?loc ntn (l,ll) l2') key)
end
| SynDefRule kn ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in
let l1 =
List.rev_map (fun (c,(subentry,(scopt,scl))) ->
@@ -493,7 +496,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
|None -> raise No_match
in
assert (List.is_empty substlist);
- mkPat ?loc qid (List.rev_append l1 l2')
+ insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
and extern_notation_pattern allscopes vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
@@ -1131,12 +1134,15 @@ and extern_notation (custom,scopes as allscopes) vars t = function
binderlists in
insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
| SynDefRule kn ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
terms in
let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
- CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
+ insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
if List.is_empty args then e
else
let args = fill_arg_scopes args argsscopes allscopes in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6b22261a15..02db8f6aab 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -120,6 +120,9 @@ type internalization_error =
| UnboundFixName of bool * Id.t
| NonLinearPattern of Id.t
| BadPatternsNumber of int * int
+ | NotAProjection of qualid
+ | NotAProjectionOf of qualid * qualid
+ | ProjectionsOfDifferentRecords of qualid * qualid
exception InternalizationError of internalization_error Loc.located
@@ -145,6 +148,16 @@ let explain_bad_patterns_number n1 n2 =
str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
str " but found " ++ int n2
+let explain_field_not_a_projection field_id =
+ pr_qualid field_id ++ str ": Not a projection"
+
+let explain_field_not_a_projection_of field_id inductive_id =
+ pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id
+
+let explain_projections_of_diff_records inductive1_id inductive2_id =
+ str "This record contains fields of both " ++ pr_qualid inductive1_id ++
+ str " and " ++ pr_qualid inductive2_id
+
let explain_internalization_error e =
let pp = match e with
| VariableCapture (id,id') -> explain_variable_capture id id'
@@ -153,6 +166,11 @@ let explain_internalization_error e =
| UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
| NonLinearPattern id -> explain_non_linear_pattern id
| BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
+ | NotAProjection field_id -> explain_field_not_a_projection field_id
+ | NotAProjectionOf (field_id, inductive_id) ->
+ explain_field_not_a_projection_of field_id inductive_id
+ | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) ->
+ explain_projections_of_diff_records inductive1_id inductive2_id
in pp ++ str "."
let error_bad_inductive_type ?loc =
@@ -719,7 +737,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
try
let gc = intern nenv c in
- Id.Map.add id (gc, Some c) map
+ Id.Map.add id (gc, None) map
with Nametab.GlobalizationError _ -> map
in
let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
@@ -1281,6 +1299,10 @@ let check_duplicate loc fields =
user_err ?loc (str "This record defines several times the field " ++
pr_qualid r ++ str ".")
+let inductive_of_record loc record =
+ let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in
+ Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive
+
(** [sort_fields ~complete loc fields completer] expects a list
[fields] of field assignments [f = e1; g = e2; ...], where [f, g]
are fields of a record and [e1] are "values" (either terms, when
@@ -1303,8 +1325,7 @@ let sort_fields ~complete loc fields completer =
let gr = global_reference_of_reference first_field_ref in
(gr, Recordops.find_projection gr)
with Not_found ->
- user_err ?loc ~hdr:"intern"
- (pr_qualid first_field_ref ++ str": Not a projection")
+ raise (InternalizationError(loc, NotAProjection first_field_ref))
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1363,12 +1384,18 @@ let sort_fields ~complete loc fields completer =
with Not_found ->
user_err ?loc ~hdr:"intern"
(str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
+ let this_field_record = try Recordops.find_projection field_glob_ref
+ with Not_found ->
+ let inductive_ref = inductive_of_record loc record in
+ raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref)))
+ in
let remaining_projs, (field_index, _) =
let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
- user_err ?loc
- (str "This record contains fields of different records.")
+ let ind1 = inductive_of_record loc record in
+ let ind2 = inductive_of_record loc this_field_record in
+ raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
in
index_fields fields remaining_projs ((field_index, field_value) :: acc)
| [] ->
@@ -2024,15 +2051,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (ltacvars, ntnvars) = lvar in
(* Preventively declare notation variables in ltac as non-bindings *)
Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars;
- let ntnvars = Id.Map.domain ntnvars in
let extra = ltacvars.ltac_extra in
+ (* We inform ltac that the interning vars and the notation vars are bound *)
+ (* but we could instead rely on the "intern_sign" *)
let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
- let lvars = Id.Set.union lvars ntnvars in
+ let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
let ltacvars = Id.Set.union lvars env.ids in
+ (* Propagating enough information for mutual interning with tac-in-term *)
+ let intern_sign = {
+ Genintern.intern_ids = env.ids;
+ Genintern.notation_variable_status = ntnvars
+ } in
let ist = {
Genintern.genv = globalenv;
ltacvars;
extra;
+ intern_sign;
} in
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
@@ -2317,16 +2351,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
~pattern_mode:true ~ltacvars env sigma c in
pattern_of_glob_constr c
+let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
+ { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
+ let tmp_scope = scope_of_type_kind sigma kind in
+ let impls = empty_internalization_env in
+ internalize env {ids; unb = false; tmp_scope; scopes = []; impls}
+ pattern_mode (ltacvars, vl) c
+
let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
+ let ids = extract_ids env in
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
- let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
- tmp_scope = None; scopes = []; impls = impls}
+ let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls}
false (empty_ltac_sign, vl) a in
+ (* Splits variables into those that are binding, bound, or both *)
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a, reversible = notation_constr_of_glob_constr nenv c in
- (* Splits variables into those that are binding, bound, or both *)
(* binding and bound *)
let out_scope = function None -> None,[] | Some (a,l) -> a,l in
let unused = match reversible with NonInjective ids -> ids | _ -> [] in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index dd0944cc48..147a903fe2 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -185,6 +185,13 @@ val interp_notation_constr : env -> ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
(bool * subscopes) Id.Map.t * notation_constr * reversibility_status
+(** Idem but to glob_constr (weaker check of binders) *)
+
+val intern_core : typing_constraint ->
+ env -> evar_map -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
+ Genintern.intern_variable_status -> constr_expr ->
+ glob_constr
+
(** Globalization options *)
val parsing_explicit : bool ref
diff --git a/interp/declare.ml b/interp/declare.ml
index 7a32018c0e..fe8fc7c969 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -219,7 +219,7 @@ let cache_variable ((sp,_),o) =
let (body, uctx), () = Future.force de.const_entry_body in
let poly, univs = match de.const_entry_universes with
| Monomorphic_const_entry uctx -> false, uctx
- | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
+ | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
in
let univs = Univ.ContextSet.union uctx univs in
(** We must declare the universe constraints before type-checking the
@@ -339,7 +339,7 @@ let infer_inductive_subtyping mind_ent =
match mind_ent.mind_entry_universes with
| Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
mind_ent
- | Cumulative_ind_entry cumi ->
+ | Cumulative_ind_entry (_, cumi) ->
begin
let env = Global.env () in
(* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
@@ -366,14 +366,14 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
| Monomorphic_ind_entry _ ->
(** Global constraints already defined through the inductive *)
Monomorphic_const_entry Univ.ContextSet.empty
- | Polymorphic_ind_entry ctx ->
- Polymorphic_const_entry ctx
- | Cumulative_ind_entry ctx ->
- Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+ | Polymorphic_ind_entry (nas, ctx) ->
+ Polymorphic_const_entry (nas, ctx)
+ | Cumulative_ind_entry (nas, ctx) ->
+ Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx)
in
let term, types = match univs with
| Monomorphic_const_entry _ -> term, types
- | Polymorphic_const_entry ctx ->
+ | Polymorphic_const_entry (_, ctx) ->
let u = Univ.UContext.instance ctx in
Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
in
@@ -520,7 +520,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
let declare_univ_binders gr pl =
if Global.is_polymorphic gr then
- UnivNames.register_universe_binders gr pl
+ ()
else
let l = match gr with
| ConstRef c -> Label.to_id @@ Constant.label c
diff --git a/interp/declare.mli b/interp/declare.mli
index 02e73cd66c..468e056909 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Libnames
open Constr
open Entries
open Decl_kinds
@@ -29,7 +28,7 @@ type section_variable_entry =
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
-val declare_variable : variable -> variable_declaration -> object_name
+val declare_variable : variable -> variable_declaration -> Libobject.object_name
(** Declaration of global constructions
i.e. Definition/Theorem/Axiom/Parameter/... *)
@@ -69,7 +68,7 @@ val set_declare_scheme :
(** [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
the whole block and a boolean indicating if it is a primitive record. *)
-val declare_mind : mutual_inductive_entry -> object_name * bool
+val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
(** Declaration messages *)
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 0e44a8b467..eeda5a6867 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Names
-open CErrors
open Util
open Term
open Constr
@@ -17,17 +15,10 @@ open Vars
open Declarations
open Cooking
open Entries
-open Context.Rel.Declaration
(********************************)
(* Discharging mutual inductive *)
-let detype_param =
- function
- | LocalAssum (Name id, p) -> id, LocalAssumEntry p
- | LocalDef (Name id, p,_) -> id, LocalDefEntry p
- | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
-
(* Replace
Var(y1)..Var(yq):C1..Cq |- Ij:Bj
@@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds =
(* To be sure to be the same as before, should probably be moved to process_inductive *)
let params' = let (_,arity,_,_,_) = List.hd inds' in
let (params,_) = decompose_prod_n_assum nparamdecls' arity in
- List.map detype_param params
+ params
in
let ind'' =
List.map
@@ -88,13 +79,15 @@ let process_inductive info modlist mib =
| Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
| Polymorphic_ind auctx ->
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let nas = Univ.AUContext.names auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Polymorphic_ind_entry auctx
+ subst, Polymorphic_ind_entry (nas, auctx)
| Cumulative_ind cumi ->
let auctx = Univ.ACumulativityInfo.univ_context cumi in
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let nas = Univ.AUContext.names auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
+ subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx)
in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
let inds =
diff --git a/interp/genintern.ml b/interp/genintern.ml
index d9a0db040a..1b736b7977 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -14,16 +14,31 @@ open Genarg
module Store = Store.Make ()
+type intern_variable_status = {
+ intern_ids : Id.Set.t;
+ notation_variable_status :
+ (bool ref * Notation_term.subscopes option ref *
+ Notation_term.notation_var_internalization_type)
+ Id.Map.t
+}
+
type glob_sign = {
ltacvars : Id.Set.t;
genv : Environ.env;
extra : Store.t;
+ intern_sign : intern_variable_status;
+}
+
+let empty_intern_sign = {
+ intern_ids = Id.Set.empty;
+ notation_variable_status = Id.Map.empty;
}
let empty_glob_sign env = {
ltacvars = Id.Set.empty;
genv = env;
extra = Store.empty;
+ intern_sign = empty_intern_sign;
}
(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
diff --git a/interp/genintern.mli b/interp/genintern.mli
index f4f064bcac..4100f39029 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -14,10 +14,19 @@ open Genarg
module Store : Store.S
+type intern_variable_status = {
+ intern_ids : Id.Set.t;
+ notation_variable_status :
+ (bool ref * Notation_term.subscopes option ref *
+ Notation_term.notation_var_internalization_type)
+ Id.Map.t
+}
+
type glob_sign = {
ltacvars : Id.Set.t;
genv : Environ.env;
extra : Store.t;
+ intern_sign : intern_variable_status;
}
val empty_glob_sign : Environ.env -> glob_sign
diff --git a/interp/impargs.ml b/interp/impargs.ml
index ce33cb8731..d8582d856e 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -450,13 +450,13 @@ let compute_mib_implicits flags kn =
(Array.mapi (* No need to lift, arities contain no de Bruijn *)
(fun i mip ->
(** No need to care about constraints here *)
- let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
+ let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
mib.mind_packets) in
let env_ar = Environ.push_rel_context ar env in
let imps_one_inductive i mip =
let ind = (kn,i) in
- let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
+ let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in
((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
Array.mapi (fun j c ->
(ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
@@ -694,7 +694,7 @@ let declare_manual_implicits local ref ?enriching l =
let flags = !implicit_args in
let env = Global.env () in
let sigma = Evd.from_env env in
- let t, _ = Global.type_of_global_in_context env ref in
+ let t, _ = Typeops.type_of_global_in_context env ref in
let t = of_constr t in
let enriching = Option.default flags.auto enriching in
let autoimpls = compute_auto_implicits env sigma flags enriching t in
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 3668455aeb..aa20bda705 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,8 +3,8 @@ Genredexpr
Redops
Tactypes
Stdarg
-Genintern
Notation_term
+Genintern
Notation_ops
Notation
Syntax_def
diff --git a/interp/modintern.ml b/interp/modintern.ml
index c27cc9cc07..60056dfd90 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,15 +61,54 @@ let lookup_module_or_modtype kind qid =
let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
-let transl_with_decl env = function
+let lookup_polymorphism env base kind fqid =
+ let m = match kind with
+ | Module -> (Environ.lookup_module base env).mod_type
+ | ModType -> (Environ.lookup_modtype base env).mod_type
+ | ModAny -> assert false
+ in
+ let rec defunctor = function
+ | NoFunctor m -> m
+ | MoreFunctor (_,_,m) -> defunctor m
+ in
+ let rec aux m fqid =
+ let open Names in
+ match fqid with
+ | [] -> assert false
+ | [id] ->
+ let test (lab,obj) =
+ match Id.equal (Label.to_id lab) id, obj with
+ | false, _ | _, (SFBmodule _ | SFBmodtype _) -> None
+ | true, SFBmind mind -> Some (Declareops.inductive_is_polymorphic mind)
+ | true, SFBconst const -> Some (Declareops.constant_is_polymorphic const)
+ in
+ (try CList.find_map test m with Not_found -> false (* error later *))
+ | id::rem ->
+ let next = function
+ | MoreFunctor _ -> false (* error later *)
+ | NoFunctor body -> aux body rem
+ in
+ let test (lab,obj) =
+ match Id.equal (Label.to_id lab) id, obj with
+ | false, _ | _, (SFBconst _ | SFBmind _) -> None
+ | true, SFBmodule body -> Some (next body.mod_type)
+ | true, SFBmodtype body -> (* XXX is this valid? If not error later *)
+ Some (next body.mod_type)
+ in
+ (try CList.find_map test m with Not_found -> false (* error later *))
+ in
+ aux (defunctor m) fqid
+
+let transl_with_decl env base kind = function
| CWith_Module ({CAst.v=fqid},qid) ->
WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
| CWith_Definition ({CAst.v=fqid},udecl,c) ->
let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
let c, ectx = interp_constr env sigma c in
- begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
- | Entries.Polymorphic_const_entry ctx ->
- let inst, ctx = Univ.abstract_universes ctx in
+ let poly = lookup_polymorphism env base kind fqid in
+ begin match UState.check_univ_decl ~poly ectx udecl with
+ | Entries.Polymorphic_const_entry (nas, ctx) ->
+ let inst, ctx = Univ.abstract_universes nas ctx in
let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
let c = EConstr.to_constr sigma c in
WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
@@ -86,23 +125,24 @@ let loc_of_module l = l.CAst.loc
let rec interp_module_ast env kind m cst = match m with
| {CAst.loc;v=CMident qid} ->
let (mp,kind) = lookup_module_or_modtype kind qid in
- (MEident mp, kind, cst)
+ (MEident mp, mp, kind, cst)
| {CAst.loc;v=CMapply (me1,me2)} ->
- let me1',kind1, cst = interp_module_ast env kind me1 cst in
- let me2',kind2, cst = interp_module_ast env ModAny me2 cst in
+ let me1', base, kind1, cst = interp_module_ast env kind me1 cst in
+ let me2', _, kind2, cst = interp_module_ast env ModAny me2 cst in
let mp2 = match me2' with
| MEident mp -> mp
| _ -> error_application_to_not_path (loc_of_module me2) me2'
in
if kind2 == ModType then
error_application_to_module_type (loc_of_module me2);
- (MEapply (me1',mp2), kind1, cst)
+ (MEapply (me1',mp2), base, kind1, cst)
| {CAst.loc;v=CMwith (me,decl)} ->
- let me,kind,cst = interp_module_ast env kind me cst in
+ let me,base,kind,cst = interp_module_ast env kind me cst in
if kind == Module then error_incorrect_with_in_module m.CAst.loc;
- let decl, cst' = transl_with_decl env decl in
+ let decl, cst' = transl_with_decl env base kind decl in
let cst = Univ.ContextSet.union cst cst' in
- (MEwith(me,decl), kind, cst)
+ (MEwith(me,decl), base, kind, cst)
let interp_module_ast env kind m =
- interp_module_ast env kind m Univ.ContextSet.empty
+ let me, _, kind, cst = interp_module_ast env kind m Univ.ContextSet.empty in
+ me, kind, cst
diff --git a/interp/notation.ml b/interp/notation.ml
index 6104ab16c7..db8ee5bc18 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1314,7 +1314,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
let env = Global.env () in (*FIXME?*)
- let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+ let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
let scs,cls = compute_arguments_scope_full sigma typ in
(req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
@@ -1322,7 +1322,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
for the extra parameters of the section. Discard the classes
of the manually given scopes to avoid further re-computations. *)
let env = Global.env () in (*FIXME?*)
- let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+ let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
let l',cls = compute_arguments_scope_full sigma typ in
let l1 = List.firstn n l' in
let cls1 = List.firstn n cls in
@@ -1369,7 +1369,7 @@ let find_arguments_scope r =
let declare_ref_arguments_scope sigma ref =
let env = Global.env () in (* FIXME? *)
- let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in
+ let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in
let (scs,cls as o) = compute_arguments_scope_full sigma typ in
declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ab57176643..7a525f84a5 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -892,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
| GVar id' ->
(if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
sigma
- | _ -> anomaly (str "A term which can be a binder has to be a variable.")
+ | t ->
+ (* The term is a non-variable pattern *)
+ raise No_match
with Not_found ->
(* The matching against a term allowing to find the instance has not been found yet *)
(* If it will be a different name, we shall unfortunately fail *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 13:39:46 +0000