diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 6 | ||||
| -rw-r--r-- | interp/constrextern.ml | 191 | ||||
| -rw-r--r-- | interp/constrintern.ml | 34 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 21 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 4 |
5 files changed, 172 insertions, 84 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 1d51109b7f..4bdacda529 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -20,8 +20,12 @@ type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string + +type entry_level = int +type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome + type notation_entry = InConstrEntry | InCustomEntry of string -type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int +type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level type notation_key = string (* A notation associated to a given parsing rule *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0a3ee59f4e..4ec9f17c71 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -63,6 +63,28 @@ let print_universes = Detyping.print_universes (* This suppresses printing of primitive tokens (e.g. numeral) and notations *) let print_no_symbol = ref false +(* This tells to skip types if a variable has this type by default *) +let print_use_implicit_types = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Use";"Implicit";"Types"] + ~value:true + +(**********************************************************************) + +let hole = CAst.make @@ CHole (None, IntroAnonymous, None) + +let is_reserved_type na t = + not !Flags.raw_print && print_use_implicit_types () && + match na with + | Anonymous -> false + | Name id -> + try + let pat = Reserve.find_reserved_type id in + let _ = match_notation_constr false t ([],pat) in + true + with Not_found | No_match -> false + (**********************************************************************) (* Turning notations and scopes on and off for printing *) module IRuleSet = Set.Make(struct @@ -381,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args) ) impl_st +let extern_record_pattern cstrsp args = + try + if !Flags.raw_print then raise Exit; + let projs = Recordops.lookup_projections (fst cstrsp) in + if PrintingRecord.active (fst cstrsp) then + () + else if PrintingConstructor.active (fst cstrsp) then + raise Exit + else if not (get_record_print ()) then + raise Exit; + let rec ip projs args acc = + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, { CAst.v = CPatAtom None } -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + let loc = pat.CAst.loc in + (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc + | _ -> raise No_match in + ip q tail acc + | _ -> assert false + in + Some (List.rev (ip projs args [])) + with + Not_found | No_match | Exit -> None + (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try @@ -415,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in let p = - try - if !Flags.raw_print then raise Exit; - let projs = Recordops.lookup_projections (fst cstrsp) in - let rec ip projs args acc = - match projs, args with - | [], [] -> acc - | proj :: q, pat :: tail -> - let acc = - match proj, pat with - | _, { CAst.v = CPatAtom None } -> - (* we don't want to have 'x := _' in our patterns *) - acc - | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc) - | _ -> raise No_match in - ip q tail acc - | _ -> assert false - in - CPatRecord(List.rev (ip projs args [])) - with - Not_found | No_match | Exit -> + match extern_record_pattern cstrsp args with + | Some l -> CPatRecord l + | None -> let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp @@ -451,7 +485,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = in insert_pat_coercion coercion pat -and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) +and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args)) (custom, (tmp_scope, scopes) as allscopes) vars = function | NotationRule (_,ntn as specific_ntn) -> @@ -474,10 +508,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) let subscope = (subentry,(scopt,scl@scopes')) in List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in - let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in + let subscopes = find_arguments_scope gr in + let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in + let more_args = fill_arg_scopes more_args more_args_scopes allscopes in + let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else - match drop_implicits_in_patt gr nb_to_drop l2 with + if no_implicit then l2 else + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in @@ -494,10 +532,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) subst in - let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in + let subscopes = find_arguments_scope gr in + let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in + let more_args = fill_arg_scopes more_args more_args_scopes allscopes in + let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () then l2 else - match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with + if no_implicit then l2 else + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in @@ -720,7 +762,7 @@ let extern_applied_ref inctx impl (cf,f) us args = let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs = try let syndefargs = List.map (fun a -> (a,None)) syndefargs in - let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in + let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in let args = syndefargs @ extraargs in if args = [] then cf else CApp ((None, CAst.make cf), args) with Expl -> @@ -740,8 +782,10 @@ let extern_applied_notation n impl f args = if List.is_empty args then f.CAst.v else - let args = adjust_implicit_arguments false (List.length args) 1 args impl in + try + let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in mkFlattenedCApp (f,args) + with Expl -> raise No_match let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in @@ -790,6 +834,12 @@ let rec flatten_application c = match DAst.get c with end | a -> c +let same_binder_type ty nal c = + match nal, DAst.get c with + | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty' + | [], _ -> true + | _ -> assert false + (**********************************************************************) (* mapping glob_constr to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) @@ -939,12 +989,10 @@ let rec extern inctx scopes vars r = extern inctx scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_prod scopes (add_vname vars na) na bk t c + factorize_prod scopes vars na bk t c | GLambda (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_lambda inctx scopes (add_vname vars na) na bk t c + factorize_lambda inctx scopes vars na bk t c | GCases (sty,rtntypopt,tml,eqns) -> let vars' = @@ -973,17 +1021,19 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in + let eqns = List.map (extern_eqn (inctx || rtntypopt <> None) scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> - CLetTuple (List.map CAst.make nal, + let inctx = inctx || typopt <> None in + CLetTuple (List.map CAst.make nal, (Option.map (fun _ -> (make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | GIf (c,(na,typopt),b1,b2) -> + let inctx = inctx || typopt <> None in CIf (sub_extern false scopes vars c, (Option.map (fun _ -> (CAst.make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), @@ -1006,7 +1056,7 @@ let rec extern inctx scopes vars r = | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x))) in ((CAst.make fi), n, bl, extern_typ scopes vars0 ty, - extern false scopes vars1 def)) idv + sub_extern true scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) | GCoFix n -> @@ -1017,7 +1067,7 @@ let rec extern inctx scopes vars r = let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), - sub_extern false scopes vars1 bv.(i))) idv + sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) @@ -1043,7 +1093,10 @@ and extern_typ (subentry,(_,scopes)) = and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes)) -and factorize_prod scopes vars na bk aty c = +and factorize_prod scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1060,18 +1113,25 @@ and factorize_prod scopes vars na bk aty c = | _ -> CProdN ([binder],b)) | _ -> assert false) | _, _ -> - let c = extern_typ scopes vars c in - match na, c.v with + let c' = extern_typ scopes vars c in + match na, c'.v with | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + when binding_kind_eq bk bk' + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let ty = if implicit_type then ty else aty in + CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b) | _, CProdN (bl,b) -> - CProdN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CProdN (CLocalAssum([make na],Default bk,ty)::bl,b) | _, _ -> - CProdN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CProdN ([CLocalAssum([make na],Default bk,ty)],c') -and factorize_lambda inctx scopes vars na bk aty c = +and factorize_lambda inctx scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1088,16 +1148,20 @@ and factorize_lambda inctx scopes vars na bk aty c = | _ -> CLambdaN ([binder],b)) | _ -> assert false) | _, _ -> - let c = sub_extern inctx scopes vars c in - match c.v with + let c' = sub_extern inctx scopes vars c in + match c'.v with | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_name na ty) (* avoid na in ty escapes scope *) -> + when binding_kind_eq bk bk' + && not (occur_name na ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let aty = if implicit_type then ty else aty in CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) | CLambdaN (bl,b) -> - CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b) | _ -> - CLambdaN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CLambdaN ([CLocalAssum([make na],Default bk,ty)],c') and extern_local_binder scopes vars = function [] -> ([],[],[]) @@ -1111,15 +1175,17 @@ and extern_local_binder scopes vars = function Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (na,bk,ty) -> + let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) - when constr_expr_eq ty ty' && + when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, CLocalAssum(CAst.make na::nal,k,ty')::l) | (assums,ids,l) -> + let ty = if implicit_type then hole else ty in (na::assums,na::ids, CLocalAssum([CAst.make na],Default bk,ty) :: l)) @@ -1163,24 +1229,21 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [], [] in (* Adjust to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match n with - | Some n when nallargs >= n && nallargs > 0 -> + | Some n when nallargs >= n -> let args1, args2 = List.chop n args in let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in - let args2impls = try List.skipn n argsimpls with Failure _ -> [] in - (* Note: NApp(NRef f,[]), hence n=0, encodes @f *) - (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), - args2, args2scopes, args2impls - | None when nallargs > 0 -> + let args2impls = + if n = 0 then + (* Note: NApp(NRef f,[]), hence n=0, encodes @f and + conventionally deactivates implicit arguments *) + [] + else try List.skipn n argsimpls with Failure _ -> [] in + DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls + | None -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] end - | Some 0 when nallargs = 0 -> - begin match DAst.get f with - | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], [] - | _ -> t, [], [], [] - end - | None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1cfd50e26e..c39e61083d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -637,6 +637,14 @@ let rec expand_binders ?loc mk bl c = (**********************************************************************) (* Syntax extensions *) +let check_not_notation_variable f ntnvars = + (* Check bug #4690 *) + match DAst.get f with + | GVar id when Id.Map.mem id ntnvars -> + user_err (str "Prefix @ is not applicable to notation variables.") + | _ -> + () + let option_mem_assoc id = function | Some (id',c) -> Id.equal id id' | None -> false @@ -1071,11 +1079,11 @@ let find_appl_head_data c = c, impls, scopes, [] | GApp (r, l) -> begin match DAst.get r with - | GRef (ref,_) when l != [] -> + | GRef (ref,_) -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - c, List.map (drop_first_implicits n) impls, + c, (if n = 0 then [] else List.map (drop_first_implicits n) impls), List.skipn_at_least n scopes,[] | _ -> c,[],[],[] end @@ -1659,10 +1667,11 @@ let drop_notations_pattern looked_for genv = let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, [], List.map2 (in_pat_sc scopes) argscs pats) - | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *) + | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *) test_kind top g; let () = assert (List.is_empty vars) in - Some (g, List.map (in_pat false scopes) pats, []) + let (_,argscs) = find_remaining_scopes [] pats g in + Some (g, List.map2 (in_pat_sc scopes) argscs pats, []) | NApp (NRef g,args) -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; @@ -1680,7 +1689,7 @@ let drop_notations_pattern looked_for genv = test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; let (_,argscs) = find_remaining_scopes [] pats g in - Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) + Some (g,[],List.map2 (in_pat_sc scopes) argscs pats) with Not_found -> None and in_pat top scopes pt = let open CAst in @@ -1780,7 +1789,15 @@ let drop_notations_pattern looked_for genv = let (argscs1,argscs2) = find_remaining_scopes pl args g in let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in let pl = add_local_defs_and_check_length loc genv g pl args in - DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) + let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in + let pat = + if List.length pl = 0 then + (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then + implicit arguments are not inherited *) + RCPatCstr (g, pl @ args, []) + else + RCPatCstr (g, pl, args) in + DAst.make ?loc @@ pat | NList (x,y,iter,terminator,revert) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -2054,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref in + check_not_notation_variable f ntnvars; (* Rem: GApp(_,f,[]) stands for @f *) if args = [] then DAst.make ?loc @@ GApp (f,[]) else smart_gapp f loc (intern_args env args_scopes (List.map fst args)) @@ -2070,9 +2088,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref - | CNotation (_,ntn,([],[],[],[])) -> + | CNotation (_,ntn,ntnargs) -> assert (Option.is_empty isproj); - let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in + let c = intern_notation intern env ntnvars loc ntn ntnargs in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d1eb50d370..59a58d643c 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1364,35 +1364,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert = let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with - | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) - | PatVar Anonymous, NHole _ -> sigma,(0,[]) + | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[]) + | PatVar Anonymous, NHole _ -> sigma,(false,0,[]) | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 -> let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in - sigma,(0,l) + sigma,(false,0,l) | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in - if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 + if le2 > List.length l1 then raise No_match else let l1',more_args = Util.List.chop le2 l1 in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) + (* Convention: notations to @f don't keep implicit arguments *) + let no_implicit = le2 = 0 in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args) | r1, NList (x,y,iter,termin,revert) -> (match_cases_pattern_list (match_cases_pattern_no_more_args) - metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[]) + metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = match match_cases_pattern metas sigma a1 a2 with - | out,(_,[]) -> out + | out,(_,_,[]) -> out | _ -> raise No_match let match_ind_pattern metas sigma ind pats a2 = match a2 with | NRef (GlobRef.IndRef r2) when eq_ind ind r2 -> - sigma,(0,pats) + sigma,(false,0,pats) | NApp (NRef (GlobRef.IndRef r2),l2) when eq_ind ind r2 -> let le2 = List.length l2 in @@ -1401,7 +1403,8 @@ let match_ind_pattern metas sigma ind pats a2 = raise No_match else let l1',more_args = Util.List.chop le2 pats in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) + let no_implicit = le2 = 0 in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args) |_ -> raise No_match let reorder_canonically_substitution terms termlists metas = diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index c62dac013b..2ab8b620df 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -69,12 +69,12 @@ val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> val match_notation_constr_cases_pattern : 'a cases_pattern_g -> interpretation -> (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * - (int * 'a cases_pattern_g list) + (bool * int * 'a cases_pattern_g list) val match_notation_constr_ind_pattern : inductive -> 'a cases_pattern_g list -> interpretation -> (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * - (int * 'a cases_pattern_g list) + (bool * int * 'a cases_pattern_g list) (** {5 Matching a notation pattern against a [glob_constr]} *) |