- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to

  change the default pretty-printing to use Π, λ instead of
  forall and fun (and allow "," as well as "=>" for "fun" to be more
  consistent with the standard forall and exists syntax). Parsing allows
  theses new forms too, even if not in -unicode, and does not make Π or
  λ keywords. As usual, criticism and suggestions are welcome :)
  Not sure what to do about "->"/"→" ?
- [setoid_replace by] now uses tactic3() to get the right parsing level
  for tactics. 
- Type class [Instance] names are now mandatory.
- Document [rewrite at/by] and fix parsing of occs to support their
  combination.
- Backtrack on [Enriching] modifier, now used exclusively in the 
  implementation of implicit arguments.


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

1 files changed, 14 insertions, 24 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4eafbd68c..2efe88c0c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -495,49 +495,39 @@ GEXTEND Gram
 	  VernacContext c
 	    
       | global = [ IDENT "Global" -> true | -> false ];
-	 IDENT "Instance"; name = OPT identref; sup = OPT [ l = binders_let -> l ];
-(* 	 name' = OPT [ "=>"; id = identref -> id ]; *)
-	 ":" ; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
+	 IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
+	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
-	   let sup = match sup with None -> [] | Some l -> l in
-	   let is = (* We reverse the default binding mode on the right *)
-	     let n = 
-	       match name with
-		 | Some (loc, id) -> (loc, Name id)
-		 | None -> (dummy_loc, Anonymous)
-	     in
-	       n, expl, t 
+	   let sup =
+	     match sup with
+		 None -> []
+	       | Some l -> l
 	   in
-	     VernacInstance (global, sup, is, props, pri)
+	   let n = 
+	     let (loc, id) = name in 
+	       (loc, Name id)
+	   in
+	     VernacInstance (global, sup, (n, expl, t), props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
       (* Implicit *)
-      | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ];
+      | IDENT "Implicit"; IDENT "Arguments"; 
 	   local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ]; 
 	   qid = global; 
 	   pos = OPT [ "["; l = LIST0 implicit_name; "]" -> 
-		   List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
-	   VernacDeclareImplicits (local,qid,enrich,pos)
+	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
+	   VernacDeclareImplicits (local,qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
-
-(*   typeclass_ctx:  *)
-(*     [ [ sup = LIST1 operconstr SEP "->"; "=>" -> sup *)
-(*     ] ] *)
-(*   ; *)
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
     | id = ident -> (id,false,false)
     | "["; "!"; id = ident; "]" -> (id,true,true) 
     | "["; id = ident; "]" -> (id,true, false) ] ]
   ;
-(*   typeclass_param_type: *)
-(*     [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t  *)
-(*     | id = identref -> id, CHole (loc, None) ] ] *)
-(*   ; *)
   typeclass_field_type:
     [ [ id = identref; oc = of_type_with_opt_coercion; t = lconstr -> id, oc, t ] ]
   ;