Ajout de la possibilité de faire référence dans certains cas à un nom

par sa notation (p.ex. pour unfold ou pour lazy delta). 
Ex: Goal 3+4 = 7. unfold "+". 



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7

17 files changed, 150 insertions, 59 deletions

diff --git a/CHANGES b/CHANGES
index 48a3123668..1c13955429 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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)