Improving abbreviations/notations + backtrack of semantic change in r12439

- Deactivation of short names registration and printing for
  abbreviations to identical names, what avoids printing uselessly
  qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
  inserted implicit arguments at all at the time of the abbreviation
  and use the regular internalization strategy to have them inserted
  at use time.
- The previous modifications altogether make redirections of
  qualified names easier and avoid the semantic change of r12349 and
  hence allows to keep "Notation b := @a" as it was before, i.e.  as a
  notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
  redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
  abreviations for constructors in constrintern.ml + bad reverting of
  notations with holes that captured non anonymous variables in
  match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
  and for reverting printing for abbreviations to constructors applied
  to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.

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

1 files changed, 17 insertions, 7 deletions

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index b0e27f04e..245ed0f50 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -38,15 +38,25 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
   add_syntax_constant kn pat;
   Nametab.push_syndef (Nametab.Until i) sp kn
 
+let is_alias_of_already_visible_name sp = function
+  | _,ARef ref ->
+      let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in
+      dir = empty_dirpath && id = basename sp
+  | _ ->
+      false
+
 let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
-  Nametab.push_syndef (Nametab.Exactly i) sp kn;
-  if not onlyparse then
-    (* Redeclare it to be used as (short) name in case an other (distfix)
-       notation was declared inbetween *)
-    Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+  if not (is_alias_of_already_visible_name sp pat) then begin
+    Nametab.push_syndef (Nametab.Exactly i) sp kn;
+    if not onlyparse then
+      (* Redeclare it to be used as (short) name in case an other (distfix)
+	 notation was declared inbetween *)
+      Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+  end
 
 let cache_syntax_constant d =
-  load_syntax_constant 1 d
+  load_syntax_constant 1 d;
+  open_syntax_constant 1 d
 
 let subst_syntax_constant (subst,(local,pat,onlyparse)) =
   (local,subst_interpretation subst pat,onlyparse)
@@ -72,5 +82,5 @@ let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
-let search_syntactic_definition loc kn =
+let search_syntactic_definition kn =
   out_pat (KNmap.find kn !syntax_table)