diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 21 | ||||
| -rw-r--r-- | interp/genarg.ml | 2 | ||||
| -rw-r--r-- | interp/genarg.mli | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 42 | ||||
| -rw-r--r-- | interp/notation.mli | 3 | ||||
| -rw-r--r-- | lib/util.ml | 5 | ||||
| -rw-r--r-- | lib/util.mli | 1 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 16 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 14 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 1 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 8 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 18 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 63 |
17 files changed, 150 insertions, 59 deletions
@@ -39,6 +39,7 @@ Tactics expressions with explicit occurrences of match or fix. - Better heuristic of lemma unfolding for apply/eapply. - New tactics "eapply in", "erewrite", "erewrite in". +- Unfoldable references can be given by notation rather than by name in unfold. Changes from V8.1gamma to V8.1 ============================== diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index f55eee07d5..76b71be425 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1567,7 +1567,7 @@ and fTACTIC_COM = function fFORMULA x1 ++ fNODE "exact_no_check" 1 | CT_vm_cast_no_check(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "vm_cast_no_check" 1 | CT_exists(x1) -> fSPEC_LIST x1 ++ diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 1ac99efcb2..110ba8243b 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -197,6 +197,10 @@ let xlate_int_or_var_opt_to_int_opt = function | Some (ArgVar _) -> xlate_error "int_or_var: TODO" | None -> CT_coerce_NONE_to_INT_OPT CT_none +let apply_or_by_notation f = function + | AN x -> f x + | ByNotation _ -> xlate_error "TODO: ByNotation" + let tac_qualid_to_ct_ID ref = CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref))) @@ -600,14 +604,15 @@ let strip_targ_intropatt = | _ -> xlate_error "strip_targ_intropatt";; let get_flag r = - let conv_flags, red_ids = + let conv_flags, red_ids = + let csts = List.map (apply_or_by_notation tac_qualid_to_ct_ID) r.rConst in if r.rDelta then - [CT_delta], CT_unfbut (List.map tac_qualid_to_ct_ID r.rConst) + [CT_delta], CT_unfbut csts else (if r.rConst = [] then (* probably useless: just for compatibility *) [] else [CT_delta]), - CT_unf (List.map tac_qualid_to_ct_ID r.rConst) in + CT_unf csts in let conv_flags = if r.rBeta then CT_beta::conv_flags else conv_flags in let conv_flags = if r.rIota then CT_iota::conv_flags else conv_flags in let conv_flags = if r.rZeta then CT_zeta::conv_flags else conv_flags in @@ -670,9 +675,11 @@ let xlate_using = function | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);; let xlate_one_unfold_block = function - ([],qid) -> CT_coerce_ID_to_UNFOLD(tac_qualid_to_ct_ID qid) + ([],qid) -> + CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid) | (n::nums, qid) -> - CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_or_var_to_int_ne_list n nums) + CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid, + nums_or_var_to_int_ne_list n nums) ;; let xlate_with_names = function @@ -1164,8 +1171,8 @@ and xlate_tac = | TacDecompose ([],c) -> xlate_error "Decompose : empty list of identifiers?" | TacDecompose (id::l,c) -> - let id' = tac_qualid_to_ct_ID id in - let l' = List.map tac_qualid_to_ct_ID l in + let id' = apply_or_by_notation tac_qualid_to_ct_ID id in + let l' = List.map (apply_or_by_notation tac_qualid_to_ct_ID) l in CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c) | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c) | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c) diff --git a/interp/genarg.ml b/interp/genarg.ml index 303278f18d..2e057e438b 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -44,6 +44,8 @@ type argument_type = | ExtraArgType of string type 'a and_short_name = 'a * identifier located option +type 'a or_by_notation = AN of 'a | ByNotation of loc * string + type rawconstr_and_expr = rawconstr * constr_expr option (* Dynamics but tagged by a type expression *) diff --git a/interp/genarg.mli b/interp/genarg.mli index 3530bd27ce..db078bfc1e 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -18,6 +18,8 @@ open Term type 'a and_short_name = 'a * identifier located option +type 'a or_by_notation = AN of 'a | ByNotation of loc * string + (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) (* in the environment by the effective calls to Intro, Inversion, etc *) (* The [constr_expr] field is [None] in TacDef though *) @@ -156,7 +158,7 @@ val rawwit_constr : (constr_expr,rlevel) abstract_argument_type val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type val wit_constr : (constr,tlevel) abstract_argument_type -val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel) abstract_argument_type +val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation) may_eval,rlevel) abstract_argument_type val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) abstract_argument_type val wit_constr_may_eval : (constr,tlevel) abstract_argument_type @@ -180,7 +182,7 @@ val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type val wit_bindings : (constr bindings,tlevel) abstract_argument_type -val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel) abstract_argument_type +val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel) abstract_argument_type diff --git a/interp/notation.ml b/interp/notation.ml index 614c87a0cf..c31ef54ec8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -408,6 +408,8 @@ let exists_notation_in_scope scopt ntn r = r' = r with Not_found -> false +let isAVar = function AVar _ -> true | _ -> false + (**********************************************************************) (* Mapping classes to scopes *) @@ -602,21 +604,51 @@ let factorize_entries = function let is_ident s = (* Poor analysis *) String.length s <> 0 & is_letter s.[0] -let browse_notation ntn map = +let browse_notation strict ntn map = let find = if String.contains ntn ' ' then (=) ntn - else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in + else fun ntn' -> + let toks = decompose_notation_key ntn' in + let trms = List.filter (function Terminal _ -> true | _ -> false) toks in + if strict then [Terminal ntn] = trms else List.mem (Terminal ntn) trms in let l = Gmap.fold (fun scope_name sc -> Gmap.fold (fun ntn ((_,r),df) l -> if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations) map [] in - let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in - factorize_entries l + List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l + +let global_reference_of_notation test (ntn,(sc,c,_)) = + match c with + | ARef ref when test ref -> Some (ntn,sc,ref) + | AApp (ARef ref, l) when List.for_all isAVar l & test ref -> + Some (ntn,sc,ref) + | _ -> None + +let error_ambiguous_notation loc _ntn = + user_err_loc (loc,"",str "Ambiguous notation") + +let error_notation_not_reference loc ntn = + user_err_loc (loc,"", + str "Unable to interpret " ++ quote (str ntn) ++ + str " as a reference") + +let interp_notation_as_global_reference loc test ntn = + let ntns = browse_notation true ntn !scope_map in + let refs = List.map (global_reference_of_notation test) ntns in + match filter_some refs with + | [_,_,ref] -> ref + | [] -> error_notation_not_reference loc ntn + | refs -> + let f (ntn,sc,ref) = find_default ntn !scope_stack = Some sc in + match List.filter f refs with + | [_,_,ref] -> ref + | [] -> error_notation_not_reference loc ntn + | _ -> error_ambiguous_notation loc ntn let locate_notation prraw ntn = - let ntns = browse_notation ntn !scope_map in + let ntns = factorize_entries (browse_notation false ntn !scope_map) in if ntns = [] then str "Unknown notation" else diff --git a/interp/notation.mli b/interp/notation.mli index 776db1a502..8bdd8b5863 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -130,6 +130,9 @@ val level_of_notation : notation -> level (* raise [Not_found] if no level *) (*s** Miscellaneous *) +val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> + notation -> global_reference + (* Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> interpretation -> bool diff --git a/lib/util.ml b/lib/util.ml index ee373120e2..8b3fb2428b 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -778,6 +778,11 @@ let option_smartmap f a = match a with | None -> a | Some x -> let x' = f x in if x'==x then a else Some x' +let rec filter_some = function + | [] -> [] + | None::l -> filter_some l + | Some a::l -> a :: filter_some l + let map_succeed f = let rec map_f = function | [] -> [] diff --git a/lib/util.mli b/lib/util.mli index afa11d31dc..8a406519e8 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -216,6 +216,7 @@ val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> val option_iter : ('a -> unit) -> 'a option -> unit val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool val option_smartmap : ('a -> 'a) -> 'a option -> 'a option +val filter_some : 'a option list -> 'a list (* In [map_succeed f l] an element [a] is removed if [f a] raises *) (* [Failure _] otherwise behaves as [List.map f l] *) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 3cbd12e539..34cdd44d67 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -158,6 +158,10 @@ GEXTEND Gram | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr -> (Some (nl,c1), c2) ] ] ; + smart_global: + [ [ c = global -> AN c + | s = ne_string -> ByNotation (loc,s) ] ] + ; occurrences: [ [ "at"; nl = LIST1 int_or_var -> nl | -> [] ] ] @@ -166,7 +170,7 @@ GEXTEND Gram [ [ c = constr; nl = occurrences -> (nl,c) ] ] ; unfold_occ: - [ [ c = global; nl = occurrences -> (nl,c) ] ] + [ [ c = smart_global; nl = occurrences -> (nl,c) ] ] ; intropatterns: [ [ l = LIST0 simple_intropattern -> l ]] @@ -200,14 +204,14 @@ GEXTEND Gram | IDENT "delta" -> FDeltaBut [] | IDENT "iota" -> FIota | IDENT "zeta" -> FZeta - | IDENT "delta"; "["; idl = LIST1 global; "]" -> FConst idl - | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl + | IDENT "delta"; "["; idl = LIST1 smart_global; "]" -> FConst idl + | IDENT "delta"; "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl ] ] ; delta_flag: - [ [ IDENT "delta"; "["; idl = LIST1 global; "]" -> FConst idl - | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl + [ [ IDENT "delta"; "["; idl = LIST1 smart_global; "]" -> FConst idl + | IDENT "delta"; "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl ] ] ; @@ -379,7 +383,7 @@ GEXTEND Gram el = OPT eliminator -> TacNewDestruct (lc,el,ids) | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c - | IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr + | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr -> TacDecompose (l,c) (* Automation tactic *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index a797275392..523ad92fb4 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -176,7 +176,7 @@ module Tactic : val casted_open_constr : open_constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e val bindings : constr_expr bindings Gram.Entry.e - val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e + val constr_may_eval : (constr_expr,reference or_by_notation) may_eval Gram.Entry.e val quantified_hypothesis : quantified_hypothesis Gram.Entry.e val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9218fb816a..b6c38cf937 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -77,6 +77,10 @@ let pr_or_metaid pr = function let pr_and_short_name pr (c,_) = pr c +let pr_or_by_notation f = function + | AN v -> f v + | ByNotation (_,s) -> str s + let pr_located pr (loc,x) = pr x let pr_evaluable_reference = function @@ -144,11 +148,13 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x) | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> - pr_arg (pr_may_eval prc prlc prref) (out_gen rawwit_constr_may_eval x) + pr_arg (pr_may_eval prc prlc (pr_or_by_notation prref)) + (out_gen rawwit_constr_may_eval x) | QuantHypArgType -> pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x) + pr_arg (pr_red_expr (prc,prlc,pr_or_by_notation prref)) + (out_gen rawwit_red_expr x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) @@ -976,8 +982,8 @@ let rec raw_printers = drop_env pr_constr_expr, drop_env pr_lconstr_expr, pr_lpattern_expr, - drop_env pr_reference, - drop_env pr_reference, + drop_env (pr_or_by_notation pr_reference), + drop_env (pr_or_by_notation pr_reference), pr_reference, pr_or_metaid pr_lident, pr_raw_extend, diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 993f1ae622..cfa035b169 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -21,6 +21,7 @@ open Environ val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds +val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index c2571ad0ae..9b01863680 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -484,7 +484,7 @@ let rec pr_vernac = function | None -> mt() | Some r -> str"Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++ + pr_red_expr (pr_constr, pr_lconstr, pr_or_by_notation pr_reference) r ++ str" in" ++ spc() in let pr_def_body = function | DefineBody (bl,red,body,d) -> @@ -776,7 +776,7 @@ let rec pr_vernac = function let pr_mayeval r c = match r with | Some r0 -> hov 2 (str"Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_reference) r0 ++ + pr_red_expr (pr_constr,pr_lconstr,pr_or_by_notation pr_reference) r0 ++ spc() ++ str"in" ++ spc () ++ pr_constr c) | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) in diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index ef25e9b8d6..a8c975eb1f 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -55,6 +55,10 @@ let mlexpr_of_reference = function | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> +let mlexpr_of_by_notation f = function + | Genarg.AN x -> <:expr< Genarg.AN $f x$ >> + | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >> + let mlexpr_of_intro_pattern = function | Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO" | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> @@ -112,7 +116,7 @@ let mlexpr_of_red_flags { Rawterm.rIota = $mlexpr_of_bool bi$; Rawterm.rZeta = $mlexpr_of_bool bz$; Rawterm.rDelta = $mlexpr_of_bool bd$; - Rawterm.rConst = $mlexpr_of_list mlexpr_of_reference l$ + Rawterm.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$ } >> let mlexpr_of_explicitation = function @@ -155,7 +159,7 @@ let mlexpr_of_red_expr = function <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >> | Rawterm.Unfold l -> let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in - let f2 = mlexpr_of_reference in + let f2 = mlexpr_of_by_notation mlexpr_of_reference in let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in <:expr< Rawterm.Unfold $f l$ >> | Rawterm.Fold l -> diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 14794086ab..b06ec2f496 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -27,8 +27,8 @@ type raw_red_flag = | FBeta | FIota | FZeta - | FConst of reference list - | FDeltaBut of reference list + | FConst of reference or_by_notation list + | FDeltaBut of reference or_by_notation list let make_red_flag = let rec add_flag red = function @@ -255,8 +255,8 @@ and glob_tactic_expr = type raw_tactic_expr = (constr_expr, pattern_expr, - reference, - reference, + reference or_by_notation, + reference or_by_notation, reference, identifier located or_metaid, raw_tactic_expr) gen_tactic_expr @@ -264,8 +264,8 @@ type raw_tactic_expr = type raw_atomic_tactic_expr = (constr_expr, (* constr *) pattern_expr, (* pattern *) - reference, (* evaluable reference *) - reference, (* inductive *) + reference or_by_notation, (* evaluable reference *) + reference or_by_notation, (* inductive *) reference, (* ltac reference *) identifier located or_metaid, (* identifier *) raw_tactic_expr) gen_atomic_tactic_expr @@ -273,15 +273,15 @@ type raw_atomic_tactic_expr = type raw_tactic_arg = (constr_expr, pattern_expr, - reference, - reference, + reference or_by_notation, + reference or_by_notation, reference, identifier located or_metaid, raw_tactic_expr) gen_tactic_arg type raw_generic_argument = constr_expr generic_argument -type raw_red_expr = (constr_expr, reference) red_expr_gen +type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen type glob_atomic_tactic_expr = (rawconstr_and_expr, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4e0d11e508..b0e8d7322e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -373,9 +373,21 @@ let intern_or_var ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) | ArgArg _ as x -> x +let loc_of_by_notation f = function + | AN c -> f c + | ByNotation (loc,s) -> loc + +let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" + +let intern_inductive_or_by_notation = function + | AN r -> Nametab.global_inductive r + | ByNotation (loc,ntn) -> + destIndRef (Notation.interp_notation_as_global_reference loc + (function IndRef ind -> true | _ -> false) ntn) + let intern_inductive ist = function - | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) - | r -> ArgArg (Nametab.global_inductive r) + | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id) + | r -> ArgArg (intern_inductive_or_by_notation r) let intern_global_reference ist = function | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) @@ -480,29 +492,40 @@ let intern_induction_arg ist = function else ElimOnIdent (loc,id) +let evaluable_of_global_reference = function + | ConstRef c -> EvalConstRef c + | VarRef c -> EvalVarRef c + | r -> error_not_evaluable (pr_global r) + +let short_name = function + | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id) + | _ -> None + +let interp_global_reference r = + let loc,qid = qualid_of_reference r in + try locate_global qid + with Not_found -> + match r with + | Ident (loc,id) when not !strict_check -> VarRef id + | _ -> error_global_not_found_loc loc qid + +let intern_evaluable_reference_or_by_notation = function + | AN r -> evaluable_of_global_reference (interp_global_reference r) + | ByNotation (loc,ntn) -> + evaluable_of_global_reference + (Notation.interp_notation_as_global_reference loc + (function ConstRef _ | VarRef _ -> true | _ -> false) ntn) + (* Globalizes a reduction expression *) let intern_evaluable ist = function - | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id) - | Ident (_,id) when + | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id) + | AN (Ident (_,id)) when (not !strict_check & find_hyp id ist) or find_ctxvar id ist -> ArgArg (EvalVarRef id, None) | r -> - let loc,qid = qualid_of_reference r in - try - let e = match locate_global qid with - | ConstRef c -> EvalConstRef c - | VarRef c -> EvalVarRef c - | _ -> error_not_evaluable (pr_reference r) in - let short_name = match r with - | Ident (loc,id) when not !strict_check -> Some (loc,id) - | _ -> None in - ArgArg (e,short_name) - with - | Not_found -> - match r with - | Ident (loc,id) when not !strict_check -> - ArgArg (EvalVarRef id, Some (loc,id)) - | _ -> error_global_not_found_loc loc qid + let e = intern_evaluable_reference_or_by_notation r in + let na = short_name r in + ArgArg (e,na) let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) |