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

4 files changed, 90 insertions, 4 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 428583047..01eef8082 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -46,6 +46,10 @@ fun x : nat => ifn x is succ n then n else 0
      : bool
 -4
      : Z
+SUM (nat * nat) nat
+     : Set
+FST (0; 1)
+     : Z
 Nil
      : forall A : Type, list A
 NIL:list nat
@@ -57,3 +61,34 @@ Defining 'I' as keyword
      : Z * Z * Z * (Z * Z * Z)
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
      : (Z -> Z -> Z -> Z) -> Z
+plus
+     : nat -> nat -> nat
+S
+     : nat -> nat
+mult
+     : nat -> nat -> nat
+le
+     : nat -> nat -> Prop
+plus
+     : nat -> nat -> nat
+succ
+     : nat -> nat
+mult
+     : nat -> nat -> nat
+le
+     : nat -> nat -> Prop
+fun x : option Z => match x with
+                    | SOME x0 => x0
+                    | NONE => 0
+                    end
+     : option Z -> Z
+fun x : option Z => match x with
+                    | SOME2 x0 => x0
+                    | NONE2 => 0
+                    end
+     : option Z -> Z
+fun x : option Z => match x with
+                    | SOME3 x0 => x0
+                    | NONE3 => 0
+                    end
+     : option Z -> Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 8d16dff5b..f041b9b71 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -121,6 +121,18 @@ Notation "- 4" := (-2 + -2).
 Check -4.
 
 (**********************************************************************)
+(* Check preservation of scopes at printing time *)
+
+Notation SUM := sum.
+Check SUM (nat*nat) nat.
+
+(**********************************************************************)
+(* Check preservation of implicit arguments at printing time *)
+
+Notation FST := fst.
+Check FST (0;1).
+
+(**********************************************************************)
 (* Check notations for references with activated or deactivated       *)
 (* implicit arguments                                                 *)
 
@@ -159,3 +171,38 @@ Check [|1,2,3;4,5,6|].
 
 Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
 Check fun f => {| f; 0; 1; 2 |} : Z.
+
+(**********************************************************************)
+(* Check printing of notations from other modules *)
+
+(* 1- Non imported case *)
+
+Require make_notation.
+
+Check plus.
+Check S.
+Check mult.
+Check le.
+
+(* 2- Imported case *)
+
+Import make_notation.
+
+Check plus.
+Check S.
+Check mult.
+Check le.
+
+(* Check notations in cases patterns *)
+
+Notation SOME := Some.
+Notation NONE := None.
+Check (fun x => match x with SOME x => x | NONE => 0 end).
+
+Notation NONE2 := (@None _).
+Notation SOME2 := (@Some _).     
+Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
+
+Notation NONE3 := @None.
+Notation SOME3 := @Some.     
+Check (fun x => match x with SOME3 x => x | NONE3 => 0 end).
diff --git a/test-suite/prerequisite/make_notation.v b/test-suite/prerequisite/make_notation.v
index 4a75713d1..c93d102a2 100644
--- a/test-suite/prerequisite/make_notation.v
+++ b/test-suite/prerequisite/make_notation.v
@@ -1,3 +1,8 @@
 (* Used in Notation.v to test import of notations from files in sections *)
 
 Notation "'Z'" := O (at level 9).
+Notation plus := plus.
+Notation succ := S.
+Notation mult := mult (only parsing).
+Notation less := le (only parsing).
+
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 316bede93..7ddb6146d 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -49,8 +49,7 @@ Definition foo P := let '(exists x, Q) := P in x = Q :> nat.
 Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat
    (at level 200, x ident, right associativity, y at level 69).
 
-(* Check that notations to atomic references preserve implicit arguments *)
+(* This used to loop at some time before r12491 *)
 
-Notation eq := @eq.
-
-Check (eq 0 0).
+Notation R x := (@pair _ _ x).
+Check (fun x:nat*nat => match x with R x y => (x,y) end).