aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml6
-rw-r--r--interp/constrexpr_ops.mli1
-rw-r--r--interp/constrintern.ml160
-rw-r--r--interp/constrintern.mli1
-rw-r--r--interp/implicit_quantifiers.ml62
-rw-r--r--interp/notation.ml26
-rw-r--r--interp/notation.mli4
-rw-r--r--interp/notation_ops.ml4
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli1
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--interp/topconstr.ml7
12 files changed, 93 insertions, 183 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a592b4cff8..542f9feaf6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -263,12 +263,6 @@ let cases_pattern_expr_loc = function
| CPatDelimiters (loc,_,_) -> loc
| CPatCast(loc,_,_) -> loc
-let raw_cases_pattern_expr_loc = function
- | RCPatAlias (loc,_,_) -> loc
- | RCPatCstr (loc,_,_,_) -> loc
- | RCPatAtom (loc,_) -> loc
- | RCPatOr (loc,_) -> loc
-
let local_binder_loc = function
| CLocalAssum ((loc,_)::_,_,t)
| CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index f6d97e107d..b547288e3f 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -36,7 +36,6 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
val constr_loc : constr_expr -> Loc.t
val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
val local_binders_loc : local_binder_expr list -> Loc.t
(** {6 Constructors}*)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf3..2426366c62 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -430,31 +430,6 @@ let intern_assumption intern lvar env nal bk ty =
let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
env, b
-let rec free_vars_of_pat il =
- function
- | CPatCstr (loc, c, l1, l2) ->
- let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
- List.fold_left free_vars_of_pat il l2
- | CPatAtom (loc, ro) ->
- begin match ro with
- | Some (Ident (loc, i)) -> (loc, i) :: il
- | Some _ | None -> il
- end
- | CPatNotation (loc, n, l1, l2) ->
- let il = List.fold_left free_vars_of_pat il (fst l1) in
- List.fold_left (List.fold_left free_vars_of_pat) il (snd l1)
- | _ -> anomaly (str "free_vars_of_pat")
-
-let intern_local_pattern intern lvar env p =
- List.fold_left
- (fun env (loc, i) ->
- let bk = Default Implicit in
- let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in
- let n = Name i in
- let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
- env)
- env (free_vars_of_pat [] p)
-
let glob_local_binder_of_extended = function
| GLocalAssum (loc,na,bk,t) -> (na,bk,None,t)
| GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t)
@@ -482,13 +457,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
| Some ty -> ty
| None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
in
- let env = intern_local_pattern intern lvar env p in
- let il = List.map snd (free_vars_of_pat [] p) in
- let cp =
+ let il,cp =
match !intern_cases_pattern_fwd (None,env.scopes) p with
- | (_, [(_, cp)]) -> cp
+ | (il, [(subst,cp)]) ->
+ if not (Id.Map.equal Id.equal subst Id.Map.empty) then
+ user_err ~loc (str "Unsupported nested \"as\" clause.");
+ il,cp
| _ -> assert false
in
+ let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
let ienv = Id.Set.elements env.ids in
let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
let na = (loc, Name id) in
@@ -855,9 +832,9 @@ let intern_qualid loc qid intern env lvar us args =
| Some _, GApp (loc, GRef (loc', ref, None), arg) ->
GApp (loc, GRef (loc', ref, us), arg)
| Some _, _ ->
- user_err ~loc (str "Notation " ++ pr_qualid qid ++
- str " cannot have a universe instance, its expanded head
- does not start with a reference")
+ user_err ~loc (str "Notation " ++ pr_qualid qid
+ ++ str " cannot have a universe instance,"
+ ++ str " its expanded head does not start with a reference")
in
c, projapp, args2
@@ -900,7 +877,22 @@ let interp_reference vars r =
(**********************************************************************)
(** {5 Cases } *)
-(** {6 Elemtary bricks } *)
+(** Private internalization patterns *)
+type raw_cases_pattern_expr =
+ | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
+ | RCPatCstr of Loc.t * Globnames.global_reference
+ * raw_cases_pattern_expr list * raw_cases_pattern_expr list
+ (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
+ | RCPatAtom of Loc.t * Id.t option
+ | RCPatOr of Loc.t * raw_cases_pattern_expr list
+
+let raw_cases_pattern_expr_loc = function
+ | RCPatAlias (loc,_,_) -> loc
+ | RCPatCstr (loc,_,_,_) -> loc
+ | RCPatAtom (loc,_) -> loc
+ | RCPatOr (loc,_) -> loc
+
+(** {6 Elementary bricks } *)
let apply_scope_env env = function
| [] -> {env with tmp_scope = None}, []
| sc::scl -> {env with tmp_scope = sc}, scl
@@ -930,17 +922,6 @@ let find_remaining_scopes pl1 pl2 ref =
in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
simple_adjust_scopes len_pl2 (aux (impl_list,scope_list)))
-let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
-
-let product_of_cases_patterns ids idspl =
- List.fold_right (fun (ids,pl) (ids',ptaill) ->
- (ids @ ids',
- (* Cartesian prod of the or-pats for the nth arg and the tail args *)
- List.flatten (
- List.map (fun (subst,p) ->
- List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
- idspl (ids,[Id.Map.empty,[]])
-
(* @return the first variable that occurs twice in a pattern
naive n^2 algo *)
@@ -1194,12 +1175,23 @@ let alias_of als = match als.alias_ids with
*)
+let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
+
+let product_of_cases_patterns aliases idspl =
+ List.fold_right (fun (ids,pl) (ids',ptaill) ->
+ (ids @ ids',
+ (* Cartesian prod of the or-pats for the nth arg and the tail args *)
+ List.flatten (
+ List.map (fun (subst,p) ->
+ List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
+ idspl (aliases.alias_ids,[aliases.alias_map,[]])
+
let rec subst_pat_iterator y t p = match p with
| RCPatAtom (_,id) ->
begin match id with Some x when Id.equal x y -> t | _ -> p end
| RCPatCstr (loc,id,l1,l2) ->
- RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
- List.map (subst_pat_iterator y t) l2)
+ RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
+ List.map (subst_pat_iterator y t) l2)
| RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
| RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
@@ -1216,6 +1208,14 @@ let drop_notations_pattern looked_for =
let test_kind top =
if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
in
+ (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+ let rec rcp_of_glob = function
+ | GVar (loc,id) -> RCPatAtom (loc,Some id)
+ | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
+ | GRef (loc,g,_) -> RCPatCstr (loc, g,[],[])
+ | GApp (loc,GRef (_,g,_),l) -> RCPatCstr (loc, g, List.map rcp_of_glob l,[])
+ | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr ")
+ in
let rec drop_syndef top scopes re pats =
let (loc,qid) = qualid_of_reference re in
try
@@ -1285,8 +1285,9 @@ let drop_notations_pattern looked_for =
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
| CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
- when Bigint.is_strictly_pos p ->
- fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+ when Bigint.is_strictly_pos p ->
+ let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+ rcp_of_glob pat
| CPatNotation (_,"( _ )",([a],[]),[]) ->
in_pat top scopes a
| CPatNotation (loc, ntn, fullargs,extrargs) ->
@@ -1299,7 +1300,9 @@ let drop_notations_pattern looked_for =
in_not top loc scopes (subst,substlist) extrargs c
| CPatDelimiters (loc, key, e) ->
in_pat top (None,find_delimiters_scope loc key::snd scopes) e
- | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+ | CPatPrim (loc,p) ->
+ let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes in
+ rcp_of_glob pat
| CPatAtom (loc, Some id) ->
begin
match drop_syndef top scopes id [] with
@@ -1309,8 +1312,21 @@ let drop_notations_pattern looked_for =
| CPatAtom (loc,None) -> RCPatAtom (loc,None)
| CPatOr (loc, pl) ->
RCPatOr (loc,List.map (in_pat top scopes) pl)
- | CPatCast _ ->
- assert false
+ | CPatCast (loc,_,_) ->
+ (* 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
+ 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
+ the "(c : t)" notation with user defined notations (such as
+ the pair). In the long term, we will try to support such
+ casts everywhere, and use them to print the domains of
+ lambdas in the encoding of match in constr. This check is
+ here and not in the parser because it would require
+ duplicating the levels of the [pattern] rule. *)
+ CErrors.user_err ~loc ~hdr:"drop_notations_pattern"
+ (Pp.strbrk "Casts are not supported in this pattern.")
and in_pat_sc scopes x = in_pat false (x,snd scopes)
and in_not top loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
@@ -1358,7 +1374,7 @@ let drop_notations_pattern looked_for =
let rec intern_pat genv aliases pat =
let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
- let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
+ let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in
let pl' = List.map (fun (asubst,pl) ->
(asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
ids',pl' in
@@ -1392,40 +1408,7 @@ let rec intern_pat genv aliases pat =
check_or_pat_variables loc ids (List.tl idsl);
(ids,List.flatten pl')
-(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a
- bit ad-hoc, and is due to current restrictions on casts in patterns. We
- support them 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 the "(c : t)"
- notation with user defined notations (such as the pair). In the long term, we
- will try to support such casts everywhere, and use them to print the domains
- of lambdas in the encoding of match in constr. We put this check here and not
- in the parser because it would require to duplicate the levels of the
- [pattern] rule. *)
-let rec check_no_patcast = function
- | CPatCast (loc,_,_) ->
- CErrors.user_err ~loc ~hdr:"check_no_patcast"
- (Pp.strbrk "Casts are not supported here.")
- | CPatDelimiters(_,_,p)
- | CPatAlias(_,p,_) -> check_no_patcast p
- | CPatCstr(_,_,opl,pl) ->
- Option.iter (List.iter check_no_patcast) opl;
- List.iter check_no_patcast pl
- | CPatOr(_,pl) ->
- List.iter check_no_patcast pl
- | CPatNotation(_,_,subst,pl) ->
- check_no_patcast_subst subst;
- List.iter check_no_patcast pl
- | CPatRecord(_,prl) ->
- List.iter (fun (_,p) -> check_no_patcast p) prl
- | CPatAtom _ | CPatPrim _ -> ()
-
-and check_no_patcast_subst (pl,pll) =
- List.iter check_no_patcast pl;
- List.iter (List.iter check_no_patcast) pll
-
let intern_cases_pattern genv scopes aliases pat =
- check_no_patcast pat;
intern_pat genv aliases
(drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
@@ -1434,7 +1417,6 @@ let _ =
fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
let intern_ind_pattern genv scopes pat =
- check_no_patcast pat;
let no_not =
try
drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
@@ -1448,7 +1430,7 @@ let intern_ind_pattern genv scopes pat =
let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
(with_letin,
- match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
+ match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with
| _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
| _ -> error_bad_inductive_type ~loc)
| x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x)
@@ -1772,7 +1754,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
and intern_multiple_pattern env n (loc,pl) =
let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in
check_number_of_pattern loc n pl;
- product_of_cases_patterns [] idsl_pll
+ product_of_cases_patterns empty_alias idsl_pll
(* Expands a disjunction of multiple pattern *)
and intern_disjunctive_multiple_pattern env loc n mpl =
@@ -2045,8 +2027,6 @@ let interp_binder_evars env evdref na t =
let t' = locate_if_hole (loc_of_glob_constr t) na t in
understand_tcc_evars env evdref ~expected_type:IsType t'
-open Environ
-
let my_intern_constr env lvar acc c =
internalize env acc false lvar c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 758d4e650b..fdd50c6a1e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -18,7 +18,6 @@ open Constrexpr
open Notation_term
open Pretyping
open Misctypes
-open Decl_kinds
(** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7f11c0a3b6..19c872b310 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -19,7 +19,6 @@ open Typeclasses_errors
open Pp
open Libobject
open Nameops
-open Misctypes
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -119,11 +118,6 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
| [] -> bdvars, l
in aux bound l binders
-let add_name_to_ids set na =
- match na with
- | Anonymous -> set
- | Name id -> Id.Set.add id set
-
let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
let rec vars bound vs = function
| GVar (loc,id) ->
@@ -131,61 +125,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
if Id.List.mem_assoc id vs then vs
else (id, loc) :: vs
else vs
- | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
- | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
- let vs' = vars bound vs ty in
- let bound' = add_name_to_ids bound na in
- vars bound' vs' c
- | GLetIn (loc,na,b,ty,c) ->
- let vs' = vars bound vs b in
- let vs'' = Option.fold_left (vars bound) vs' ty in
- let bound' = add_name_to_ids bound na in
- vars bound' vs'' c
- | GCases (loc,sty,rtntypopt,tml,pl) ->
- let vs1 = vars_option bound vs rtntypopt in
- let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
- List.fold_left (vars_pattern bound) vs2 pl
- | GLetTuple (loc,nal,rtntyp,b,c) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 b in
- let bound' = List.fold_left add_name_to_ids bound nal in
- vars bound' vs2 c
- | GIf (loc,c,rtntyp,b1,b2) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 c in
- let vs3 = vars bound vs2 b1 in
- vars bound vs3 b2
- | GRec (loc,fk,idl,bl,tyl,bv) ->
- let bound' = Array.fold_right Id.Set.add idl bound in
- let vars_fix i vs fid =
- let vs1,bound1 =
- List.fold_left
- (fun (vs,bound) (na,k,bbd,bty) ->
- let vs' = vars_option bound vs bbd in
- let vs'' = vars bound vs' bty in
- let bound' = add_name_to_ids bound na in
- (vs'',bound')
- )
- (vs,bound')
- bl.(i)
- in
- let vs2 = vars bound1 vs1 tyl.(i) in
- vars bound1 vs2 bv.(i)
- in
- Array.fold_left_i vars_fix vs idl
- | GCast (loc,c,k) -> let v = vars bound vs c in
- (match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
- | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
- and vars_pattern bound vs (loc,idl,p,c) =
- let bound' = List.fold_right Id.Set.add idl bound in
- vars bound' vs c
-
- and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
-
- and vars_return_type bound vs (na,tyopt) =
- let bound' = add_name_to_ids bound na in
- vars_option bound' vs tyopt
+ | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
in fun rt ->
let vars = List.rev (vars bound [] rt) in
List.iter (fun (id, loc) ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 90ac7f7296..7be2fe0f01 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -22,7 +22,6 @@ open Glob_ops
open Ppextend
open Context.Named.Declaration
-module NamedDecl = Context.Named.Declaration
(*i*)
(*s A scope is a set of notations; it includes
@@ -445,16 +444,20 @@ let notation_of_prim_token = function
| Numeral n -> "- "^(to_string (neg n))
| String _ -> raise Not_found
-let find_prim_token g loc p sc =
+let find_prim_token check_allowed loc p sc =
(* Try for a user-defined numerical notation *)
try
let (_,c),df = find_notation (notation_of_prim_token p) sc in
- g (Notation_ops.glob_constr_of_notation_constr loc c),df
+ let pat = Notation_ops.glob_constr_of_notation_constr loc c in
+ check_allowed pat;
+ pat, df
with Not_found ->
(* Try for a primitive numerical notation *)
let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
check_required_module loc sc spdir;
- g (interp ()), ((dirpath (fst spdir),DirPath.empty),"")
+ let pat = interp () in
+ check_allowed pat;
+ pat, ((dirpath (fst spdir),DirPath.empty),"")
let interp_prim_token_gen g loc p local_scopes =
let scopes = make_current_scopes local_scopes in
@@ -467,20 +470,17 @@ let interp_prim_token_gen g loc p local_scopes =
| String s -> str "No interpretation for string " ++ qs s) ++ str ".")
let interp_prim_token =
- interp_prim_token_gen (fun x -> x)
+ interp_prim_token_gen (fun _ -> ())
-(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
-
-let rec rcp_of_glob looked_for = function
- | GVar (loc,id) -> RCPatAtom (loc,Some id)
- | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
- | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[])
+let rec check_allowed_ref_in_pat looked_for = function
+ | GVar _ | GHole _ -> ()
+ | GRef (_,g,_) -> looked_for g
| GApp (loc,GRef (_,g,_),l) ->
- looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+ looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
| _ -> raise Not_found
let interp_prim_token_cases_pattern_expr loc looked_for p =
- interp_prim_token_gen (rcp_of_glob looked_for) loc p
+ interp_prim_token_gen (check_allowed_ref_in_pat looked_for) loc p
let interp_notation loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation.mli b/interp/notation.mli
index 2e92a00a8c..300480ff1c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module ->
val interp_prim_token : Loc.t -> prim_token -> local_scopes ->
glob_constr * (notation_location * scope_name option)
+
+(* This function returns a glob_const representing a pattern *)
val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token ->
- local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option)
+ local_scopes -> glob_constr * (notation_location * scope_name option)
(** Return the primitive token associated to a [term]/[cases_pattern];
raise [No_match] if no such token *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8b4fadb5a0..d08fb107be 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1141,10 +1141,6 @@ let term_of_binder = function
| Name id -> GVar (Loc.ghost,id)
| Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
-type glob_decl2 =
- (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
- glob_constr option * glob_constr
-
let match_notation_constr u c (metas,pat) =
let terms,binders,termlists,binderlists =
match_ false u ([],[]) metas ([],[],[],[]) c pat in
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 341ff5662c..5920b0d508 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,9 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Misctypes
-open Tactypes
open Genarg
open Geninterp
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 113fe40ba7..ac40a23281 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -10,7 +10,6 @@
open Loc
open Names
-open Term
open EConstr
open Libnames
open Globnames
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index c3f4c4f302..ed7b0b70d4 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -106,5 +106,3 @@ let search_syntactic_definition kn =
let def = out_pat pat in
verbose_compat kn def v;
def
-
-open Goptions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d3142e7f0c..e05be65fb0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -178,7 +178,12 @@ let split_at_annot bl na =
in
(List.rev ans, CLocalAssum (r, k, t) :: rest)
end
- | CLocalDef _ as x :: rest -> aux (x :: acc) rest
+ | CLocalDef ((_,na),_,_) as x :: rest ->
+ if Name.equal (Name id) na then
+ user_err ~loc
+ (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+ else
+ aux (x :: acc) rest
| CLocalPattern (loc,_,_) :: rest ->
Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
| [] ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:39:44 +0000