Syntax changes in typeclasses, remove "?" for usual implicit arguments

binding, add "!" syntax for the new binders which require parameters and
not superclasses. Change backquotes for curly braces for user-given
implicit arguments, following tradition. This requires a hack a la
lpar-id-coloneq. Change ident to global for typeclass names in class
binders. Also requires a similar hack to distinguish between [ C t1 tn ]
and [ c : C t1 tn ]. Update affected theories.

While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.

Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).


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

1 files changed, 10 insertions, 10 deletions

diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index c385fc5b5..8a435b449 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -42,7 +42,7 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70)
 
 (** Use program to solve some obligations. *)
 
-Definition swap_sumbool `A B` (x : { A } + { B }) : { B } + { A } :=
+Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
     | left H => @right _ _ H 
     | right H => @left _ _ H 
@@ -52,7 +52,7 @@ Require Import Coq.Program.Program.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -60,10 +60,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition equiv_decb [ ! EqDec A ] (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -78,15 +78,15 @@ Require Import Coq.Arith.Arith.
 Program Instance eq_setoid : Setoid A :=
   equiv := eq ; setoid_equiv := eq_equivalence.
 
-Program Instance nat_eq_eqdec : ? EqDec (@eq_setoid nat) :=
+Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) :=
   equiv_dec := eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
-Program Instance bool_eqdec : ? EqDec (@eq_setoid bool) :=
+Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
   equiv_dec := bool_dec.
 
-Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) :=
+Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
   equiv_dec x y := left.
 
   Next Obligation.
@@ -95,8 +95,8 @@ Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => 
-  prod_eqdec : ? EqDec (@eq_setoid (prod A B)) :=
+Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => 
+  prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     dest x as (x1, x2) in 
     dest y as (y1, y2) in 
@@ -111,7 +111,7 @@ Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] =>
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@eq_setoid (bool -> A)) :=
+Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then left