Switched to "standardized" names for the properties of eq and

identity. Add notations for compatibility and support for
understanding these notations in the ml files.



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

1 files changed, 9 insertions, 5 deletions

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 8f303ea61..bb8d68323 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -83,15 +83,19 @@ let declare_syntactic_definition local id onlyparse pat =
 let search_syntactic_definition loc kn =
   out_pat (KNmap.find kn !syntax_table)
 
-let locate_global_with_alias (loc,qid) =
-  match Nametab.extended_locate qid with
+let global_of_extended_global = function
   | TrueGlobal ref -> ref
   | SyntacticDef kn -> 
   match search_syntactic_definition dummy_loc kn with
   | [],ARef ref -> ref
-  | _ -> 
-      user_err_loc (loc,"",pr_qualid qid ++ 
-        str " is bound to a notation that does not denote a reference")
+  | _ -> raise Not_found
+
+let locate_global_with_alias (loc,qid) =
+  let ref = Nametab.extended_locate qid in
+  try global_of_extended_global ref
+  with Not_found ->
+    user_err_loc (loc,"",pr_qualid qid ++ 
+      str " is bound to a notation that does not denote a reference")
 
 let inductive_of_reference_with_alias r =
   match locate_global_with_alias (qualid_of_reference r) with