Changement 'as notation' en 'where notation'

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

6 files changed, 35 insertions, 45 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 49f8b0d85..0c79c9973 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -148,8 +148,8 @@ GEXTEND Gram
     [ [ ","; nal = LIST1 base_ident SEP "," -> nal | -> [] ] ]
   ;
   decl_notation:
-    [ [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc] -> 
-        (ntn,scopt) ] ]
+    [ [ "where"; ntn = STRING; ":="; c = constr; 
+         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ]
   ;
   type_option:
     [ [ ":"; c = constr -> c 
@@ -228,7 +228,7 @@ GEXTEND Gram
   ;
   oneind:
     [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
-        ntn = OPT decl_notation ; ":="; lc = constructor_list ->
+        ":="; lc = constructor_list; ntn = OPT decl_notation ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
@@ -252,7 +252,7 @@ GEXTEND Gram
   ;
   onerec:
     [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
-        ntn = OPT decl_notation; ":="; def = constr ->
+        ":="; def = constr; ntn = OPT decl_notation ->
           let ni = List.length (List.flatten (List.map fst bl)) - 1 in
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 7475566b7..3955d15f8 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -28,7 +28,7 @@ open Vernac_
 open Module
 
 
-let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..." ]
+let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..."; "where" ]
 let _ = 
   if not !Options.v7 then
     List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
@@ -181,13 +181,13 @@ GEXTEND Gram
       | -> None ] ]
   ;
   decl_notation:
-    [ [ OPT [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc]
-               -> (ntn,scopt) ] ] ]
+    [ [ OPT [ "where"; ntn = STRING; ":="; c = constr; 
+         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ]
     ;
   (* Inductives and records *)
   inductive_definition:
     [ [ id = base_ident; indpar = LIST0 binder_let; ":"; c = lconstr; 
-        ntn = decl_notation; ":="; lc = constructor_list ->
+        ":="; lc = constructor_list; ntn = decl_notation ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   constructor_list:
@@ -208,7 +208,7 @@ GEXTEND Gram
   rec_definition:
     [ [ id = base_ident; bl = LIST1 binder_nodef;
         annot = OPT rec_annotation; type_ = type_cstr; 
-	ntn = decl_notation; ":="; def = lconstr ->
+	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (List.flatten (List.map fst bl)) in
           let ni =
             match annot with
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 469a9d4bf..e32bd4205 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -27,7 +27,9 @@ Notation "~ x" := (not x) : type_scope.
 
 Hints Unfold not : core.
 
-Inductive and [A,B:Prop] : Prop as "A /\ B" := conj : A -> B -> A /\ B.
+Inductive and [A,B:Prop] : Prop := conj : A -> B -> A /\ B
+
+where "A /\ B" := (and A B) : type_scope.
 
 V7only[
 Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1).
@@ -58,9 +60,11 @@ End Conjunction.
 
 (** [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
 
-Inductive or [A,B:Prop] : Prop as "A \/ B":=
+Inductive or [A,B:Prop] : Prop :=
      or_introl : A -> A \/ B 
-   | or_intror : B -> A \/ B.
+   | or_intror : B -> A \/ B
+
+where "A \/ B" := (or A B) : type_scope.
 
 (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
 
@@ -173,8 +177,10 @@ Section universal_quantification.
     The others properties (symmetry, transitivity, replacement of 
     equals) are proved below *)
 
-Inductive eq [A:Type;x:A] : (y:A)Prop as "x = y :> A" : type_scope
-       := refl_equal : x = x :> A.
+Inductive eq [A:Type;x:A] : A->Prop
+       := refl_equal : x = x :> A
+
+where "x = y :> A" := (!eq A x y) : type_scope.
 
 Notation "x = y" := (eq ? x y) : type_scope.
 Notation "x <> y  :> T" := ~ (!eq T x y) : type_scope.
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 45af3a3c5..a1b42f7be 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -906,7 +906,7 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
       (local,(Some prec,ppprec),ppnot,Some gram_rule,pp_rule));
 
   (* Declare interpretation *)
-  let a = interp_aconstr vars c in
+  let a = interp_aconstr [] vars c in
   let old_pp_rule =
     (* Used only by v7 *)
     if onlyparse then None
@@ -940,29 +940,13 @@ let add_notation_interpretation_core local symbs for_old df a scope onlyparse
   Lib.add_anonymous_leaf
     (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,df))
 
-let check_occur l id =
-  if not (List.mem (Name id) l) then error ((string_of_id id)^"is unbound")
-
-let add_notation_interpretation df (c,l) sc =
+let add_notation_interpretation df names c sc =
   let (vars,symbs) = analyse_tokens (split df) in
-  List.iter (check_occur l) vars;
-  let a_for_old =
-    let c = match c with AVar id -> RVar (dummy_loc,id)
-      | ARef c -> RRef (dummy_loc,c)
-      | _ -> anomaly "add_notation_interpretation" in
-    RApp (dummy_loc, c,
-      List.map (function
-	| Name id when List.mem id vars -> RVar (dummy_loc,id)
-	| _ -> RHole (dummy_loc,QuestionMark)) l) in
-  let a = AApp (c,List.map (function 
-    | Name id when List.mem id vars -> AVar id
-    | _ -> AHole QuestionMark) l) in
-  let la = List.map (fun id -> id,(None,[])) vars in
-  let onlyparse = false in
-  let local = false in
+  let a = interp_aconstr names vars c in
+  let a_for_old = interp_rawconstr_with_implicits (Global.env()) vars names c 
+  in
   let for_oldpp = Some (a_for_old,vars) in
-  add_notation_interpretation_core local symbs for_oldpp df (la,a) sc
-    onlyparse false
+  add_notation_interpretation_core false symbs for_oldpp df a sc false false
 
 let add_notation_in_scope_v8only local df c mv8 scope toks =
   let (_,vars,notation),prec,ppdata = compute_syntax_data false (df,mv8) in
@@ -971,7 +955,7 @@ let add_notation_in_scope_v8only local df c mv8 scope toks =
     (inSyntaxExtension(local,(None,prec),notation,None,pp_rule));
   (* Declare the interpretation *)
   let onlyparse = false in
-  let a = interp_aconstr vars c in
+  let a = interp_aconstr [] vars c in
   Lib.add_anonymous_leaf
     (inNotation(local,None,notation,scope,a,onlyparse,true,df))
 
@@ -991,7 +975,7 @@ let add_notation_v8only local c (df,modifiers) sc =
 	        (* Declare only interpretation *)
 		let (vars,symbs) = analyse_tokens toks in
 		let onlyparse = modifiers = [SetOnlyParsing] in
-		let a = interp_aconstr vars c in
+		let a = interp_aconstr [] vars c in
 		let a_for_old = interp_global_rawconstr_with_vars vars c in
 		add_notation_interpretation_core local symbs None df a sc 
 		  onlyparse true
@@ -1014,7 +998,7 @@ let add_notation local c dfmod mv8 sc =
 	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
         (* Means a Syntactic Definition *)
         let ident = id_of_string (strip x) in
-	let c = snd (interp_aconstr [] c) in
+	let c = snd (interp_aconstr [] [] c) in
 	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
         Syntax_def.declare_syntactic_definition local ident onlyparse c
     | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
@@ -1030,7 +1014,7 @@ let add_notation local c dfmod mv8 sc =
 	        (* Declare only interpretation *)
 		let (vars,symbs) = analyse_tokens toks in
 		let onlyparse = modifiers = [SetOnlyParsing] in
-		let a = interp_aconstr vars c in
+		let a = interp_aconstr [] vars c in
 		let a_for_old = interp_global_rawconstr_with_vars vars c in
 		let for_old = Some (a_for_old,vars) in
 		add_notation_interpretation_core local symbs for_old df a
@@ -1082,7 +1066,7 @@ let add_infix local (inf,modl) pr mv8 sc =
     if a8=None & n8=None & fmt=None then
       (* Declare only interpretation *)
       let (vars,symbs) = analyse_tokens toks in
-      let a' = interp_aconstr vars a in
+      let a' = interp_aconstr [] vars a in
       let a_for_old = interp_global_rawconstr_with_vars vars a in
       add_notation_interpretation_core local symbs None df a' sc 
 	onlyparse true
@@ -1110,7 +1094,7 @@ let add_infix local (inf,modl) pr mv8 sc =
     (* de ne déclarer que l'interprétation *)
     (* Declare only interpretation *)
     let (vars,symbs) = analyse_tokens toks in
-    let a' = interp_aconstr vars a in
+    let a' = interp_aconstr [] vars a in
     let a_for_old = interp_global_rawconstr_with_vars vars a in
     let for_old = Some (a_for_old,vars) in
     add_notation_interpretation_core local symbs for_old df a' sc 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 2d1084623..74b199ed7 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -45,8 +45,8 @@ val add_notation : locality_flag -> constr_expr
   -> (string * syntax_modifier list) option
       -> scope_name option -> unit
 
-val add_notation_interpretation : string -> (aconstr * Names.name list)
-  -> scope_name option -> unit
+val add_notation_interpretation : string -> Constrintern.implicits_env
+  -> constr_expr -> scope_name option -> unit
 
 val add_syntax_extension : locality_flag
   -> (string * syntax_modifier list) option
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index beb26e41f..441244caf 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -125,7 +125,7 @@ type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
 
 type sort_expr = Rawterm.rawsort
 
-type decl_notation = (string * scope_name option) option
+type decl_notation = (string * constr_expr * scope_name option) option
 type simple_binder = identifier * constr_expr
 type 'a with_coercion = coercion_flag * 'a
 type constructor_expr = simple_binder with_coercion