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, 4 insertions, 7 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f520c4fd6..d6b4c1354 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1973,13 +1973,10 @@ Notation list := list (only parsing).
 Notation list_rect := list_rect (only parsing).
 Notation list_rec := list_rec (only parsing).
 Notation list_ind := list_ind (only parsing).
-Notation nil := @nil (only parsing).
-Notation cons := @cons (only parsing).
-Notation length := @length (only parsing).
-Notation app := @app (only parsing).
-(* We hide these compatibility notations behind the true definitions
-   that are in [Datatypes]: *)
-Export Datatypes.
+Notation nil := nil (only parsing).
+Notation cons := cons (only parsing).
+Notation length := length (only parsing).
+Notation app := app (only parsing).
 (* Compatibility Names *)
 Notation ass_app := app_assoc (only parsing).
 Notation app_ass := app_assoc_reverse (only parsing).