petits changements de syntaxe

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

17 files changed, 175 insertions, 132 deletions

diff --git a/Makefile b/Makefile
index 092c7c2c4..c2c39cbc4 100644
--- a/Makefile
+++ b/Makefile
@@ -1149,7 +1149,7 @@ GRAMMARNEEDEDCMO=\
   proofs/tacexpr.cmo parsing/ast.cmo \
   parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \
   toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_coqast.cmo \
-  parsing/egrammar.cmo 
+  parsing/egrammar.cmo
 
 CAMLP4EXTENSIONSCMO=\
   parsing/argextend.cmo parsing/tacextend.cmo parsing/vernacextend.cmo 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 87a9033f6..76f4b3611 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -157,7 +157,7 @@ let field g =
       | _ -> error "The statement is not built from Leibniz' equality" in
   let th = VConstr (lookup (pf_env g) typ) in
   (interp_tac_gen [(id_of_string "FT",th)] (get_debug ())
-    <:tactic< match context with |- (@eq _ _ _) => field_gen FT end >>) g
+    <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
 
 (* Verifies that all the terms have the same type and gives the right theory *)
 let guess_theory env evc = function
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 155a264f7..162ea2ebf 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -710,7 +710,7 @@ let declareFunScheme f fname mutflist =
 
 VERNAC COMMAND EXTEND FunctionalScheme
  [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
-    constr(c) "with" constr_list(l) ]
+    constr(c) "with" ne_constr_list(l) ]
   -> [ declareFunScheme c na l ]
 | [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" constr(c) ]
   -> [ declareFunScheme c na [] ]
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 21c95d326..5f37c2f54 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -316,8 +316,8 @@ $$
 \KWD{IF}~\notv~\KWD{then}~\notv~\KWD{else}~\notv
                      & 200R \\
 \infx{:}             & 100R \\
-\infx{\rightarrow}\quad \infx{\leftrightarrow}
-                     & 90R \\
+\infx{\leftrightarrow} & 95N \\
+\infx{\rightarrow}   & 90R \\
 \infx{\vee}          & 85R \\
 \infx{\wedge}        & 80R \\
 \tilde{}\notv        & 75R \\
@@ -404,6 +404,8 @@ $$
 \nlsep \TERM{cut}~\tacconstr
 \nlsep \TERM{assert}~\tacconstr
 \nlsep \TERM{assert}~
+  \TERM{(}~\NT{ident}~\KWD{:}~\taclconstr~\TERM{)}
+\nlsep \TERM{assert}~
   \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}
 \nlsep \TERM{pose}~\tacconstr
 \nlsep \TERM{pose}~
@@ -461,13 +463,13 @@ $$
 \nlsep \TERM{symmetry}~\OPTGR{\KWD{in}~\NT{ident}}
 \nlsep \TERM{transitivity}~\tacconstr
 %%
-\nlsep \NT{inversion-kwd}~\NT{quantified-hyp}~\NT{with-names}~\NT{clause}
+\nlsep \NT{inversion-kwd}~\NT{quantified-hyp}~\NT{with-names}~\OPT{\NT{clause}}
 \nlsep \TERM{dependent}~\NT{inversion-kwd}~\NT{quantified-hyp}
   ~\NT{with-names}~\OPTGR{\KWD{with}~\tacconstr}
-\nlsep \TERM{inversion}~\NT{quantified-hyp}~\TERM{using}~\tacconstr~\NT{clause}
+\nlsep \TERM{inversion}~\NT{quantified-hyp}~\TERM{using}~\tacconstr~\OPT{\NT{clause}}
 %%
-\nlsep \NT{red-expr}~\NT{clause}
-\nlsep \TERM{change}~\NT{conversion}~\NT{clause}
+\nlsep \NT{red-expr}~\OPT{\NT{clause}}
+\nlsep \TERM{change}~\NT{conversion}~\OPT{\NT{clause}}
 \SEPDEF
 \DEFNT{red-expr}
        \TERM{red} ~\mid~ \TERM{hnf} ~\mid~ \TERM{compute}
@@ -543,18 +545,29 @@ Conflicts exists between integers and constrs.
        \TERM{delta}~\OPT{\TERM{-}}~\TERM{[}~\PLUS{\NT{reference}}~\TERM{]}
 \SEPDEF
 \DEFNT{clause}
-       \OPTGR{\KWD{in}~\PLUS{\NT{hyp-ident}}}
+       \KWD{in}~\TERM{*}
+\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-list}} \KWD{\vdash} \OPT{\TERM{*}}
+\SEPDEF
+\DEFNT{hyp-ident-list}
+       \NT{hyp-ident}
+\nlsep \NT{hyp-ident}~\KWD{,}~\NT{hyp-ident-list}
 \SEPDEF
 \DEFNT{hyp-ident}
        \NT{ident}
 \nlsep \KWD{(}~\TERM{type}~\TERM{of}~\NT{ident}~\KWD{)}
+\nlsep \KWD{(}~\TERM{value}~\TERM{of}~\NT{ident}~\KWD{)}
 \SEPDEF
 \DEFNT{clause-pattern}
-       \KWD{in}~\NT{pattern-hyp-list}
+       \KWD{in}~\TERM{*}
+\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-occ-list}} \KWD{\vdash} \OPT{\TERM{*}}
+\SEPDEF
+\DEFNT{hyp-ident-occ-list}
+       \NT{hyp-ident-occ}
+\nlsep \NT{hyp-ident-occ}~\KWD{,}~\NT{hyp-ident-occ-list}
 \SEPDEF
-\DEFNT{pattern-hyp-list}
-       \STAR{\NT{int}}~\TERM{goal}
-\nlsep \STAR{\NT{int}}~\NT{ident}~\OPT{\NT{pattern-hyp-list}}
+\DEFNT{hyp-ident-occ}
+       \NT{hyp-ident}
+\nlsep \NT{hyp-ident}~\KWD{at}~\PLUS{\NT{int}}
 \SEPDEF
 \DEFNT{hint-bases}
        \KWD{with}~\TERM{*}
@@ -592,8 +605,8 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
        ~\NT{tactic}  &1 &\RNAME{Fun-tac}
 \nlsep \KWD{let} ~\NT{let-clauses} ~\KWD{in} ~\NT{tactic}
 \nlsep \KWD{let} ~\TERM{rec} ~\NT{rec-clauses} ~\KWD{in} ~\NT{tactic}
-\nlsep \KWD{match}~\OPT{\TERM{reverse}}~\TERM{context}~\KWD{with}
-       ~\OPT{\TERMbar}~\OPT{\NT{match-ctxt-rules}} ~\KWD{end}
+\nlsep \KWD{match}~\OPT{\TERM{reverse}}~\TERM{goal}~\KWD{with}
+       ~\OPT{\TERMbar}~\OPT{\NT{match-goal-rules}} ~\KWD{end}
 \nlsep \KWD{match} ~\NT{tactic} ~\KWD{with}
        ~\OPT{\TERMbar}~\OPT{\NT{match-rules}} ~\KWD{end}
 \nlsep \TERM{abstract}~\NT{tactic}~\OPTGR{\TERM{using}~\NT{ident}}
@@ -601,11 +614,8 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \nlsep \TERM{solve}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
 \nlsep \TERM{idtac}
 \nlsep \TERM{fail} ~\OPT{\NT{int}} ~\OPT{\NT{string}}
-\nlsep \TERM{fresh} ~\OPT{\NT{string}}
-\nlsep \TERM{context} ~\NT{ident} ~\TERM{[} ~\taclconstr ~\TERM{]}
-\nlsep \TERM{eval} ~\NT{red-expr} ~\KWD{in} ~\tacconstr
-\nlsep \TERM{type} ~\tacconstr
-\nlsep \TERM{'} ~\tacconstr
+\nlsep \TERM{constr}~\KWD{:}~\tacconstr
+\nlsep \NT{term-ltac}
 \nlsep \NT{reference}~\STAR{\NT{tactic-arg}}  &&\RNAME{call-tactic}
 \nlsep \NT{simple-tactic}
 %%
@@ -613,10 +623,17 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \nlsep \KWD{(} ~\NT{tactic} ~\KWD{)}
 \SEPDEF
 \DEFNT{tactic-arg}
-       \TERM{\bf '} ~\NTL{tactic}{0}
+       \TERM{ltac}~\KWD{:}~\NTL{tactic}{0}
+\nlsep \NT{term-ltac}
 \nlsep \NT{tactic-atom}
 \nlsep \tacconstr
 \SEPDEF
+\DEFNT{term-ltac}
+       \TERM{fresh} ~\OPT{\NT{string}}
+\nlsep \TERM{context} ~\NT{ident} ~\TERM{[} ~\taclconstr ~\TERM{]}
+\nlsep \TERM{eval} ~\NT{red-expr} ~\KWD{in} ~\tacconstr
+\nlsep \TERM{type} ~\tacconstr
+\SEPDEF
 \DEFNT{tactic-atom}
        \NT{reference}
 \nlsep \TERM{()}
@@ -634,24 +651,23 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \SEPDEF
 \DEFNT{let-clause}
        \NT{ident} ~\STAR{\NT{name}} ~\KWD{:=} ~\NT{tactic}
-\nlsep \NT{ident} ~\KWD{:} ~\tacconstr
-\nlsep \NT{ident} ~\KWD{:} ~\taclconstr ~\KWD{:=}~\TERM{proof}
-\nlsep \NT{ident} ~\KWD{:} ~\taclconstr ~\KWD{:=} ~\NT{tactic}
 \SEPDEF
 \DEFNT{rec-clauses}
        \NT{rec-clause} ~\KWD{with} ~\NT{rec-clauses}
 \nlsep \NT{rec-clause}
 \SEPDEF
 \DEFNT{rec-clause}
-       \NT{ident} ~\PLUS{\NT{name}} ~\KWD{$\Rightarrow$} ~\NT{tactic}
+       \NT{ident} ~\PLUS{\NT{name}} ~\KWD{:=} ~\NT{tactic}
 \SEPDEF
-\DEFNT{match-ctxt-rules}
-       \NT{match-ctxt-rule}
-\nlsep \NT{match-ctxt-rule} ~\TERMbar ~\NT{match-ctxt-rules}
+\DEFNT{match-goal-rules}
+       \NT{match-goal-rule}
+\nlsep \NT{match-goal-rule} ~\TERMbar ~\NT{match-goal-rules}
 \SEPDEF
-\DEFNT{match-ctxt-rule}
+\DEFNT{match-goal-rule}
        \NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
        ~\KWD{$\Rightarrow$} ~\NT{tactic}
+\nlsep \KWD{[}~\NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
+       ~\KWD{]}~\KWD{$\Rightarrow$} ~\NT{tactic}
 \nlsep \KWD{_} ~\KWD{$\Rightarrow$} ~\NT{tactic}
 \SEPDEF
 \DEFNT{match-hyps-list}
@@ -698,8 +714,7 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
          ~\OPTGR{\KWD{in}~\NT{ident}}
 \nlsep \TERM{absurd} ~\tacconstr
 \nlsep \TERM{contradiction}
-\nlsep \TERM{autorewrite}~\TERM{[}~\PLUS{\NT{ident}}~\TERM{]}
-         ~\OPTGR{\KWD{using}~\NT{tactic}}
+\nlsep \TERM{autorewrite}~\NT{hint-bases}~\OPTGR{\KWD{using}~\NT{tactic}}
 \nlsep \TERM{refine}~\tacconstr
 \nlsep \TERM{setoid_replace} ~\tacconstr ~\KWD{with} ~\tacconstr
 \nlsep \TERM{setoid_rewrite} ~\NT{orient} ~\tacconstr
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index eaf039b9d..cad065329 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -79,6 +79,9 @@ let mk_fix(loc,kw,id,dcls) =
     let fb = List.map mk_cofixb dcls in
     CCoFix(loc,id,fb)
 
+let mk_single_fix (loc,kw,dcl) =
+  let (_,id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
+
 let binder_constr =
   create_constr_entry (get_univ "constr") "binder_constr"
 
@@ -197,12 +200,13 @@ GEXTEND Gram
             | LocalRawDef ((loc,_),_)::_ -> loc
             | _ -> dummy_loc in
           CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
-      | "let"; fx = fix_constr; "in"; c = operconstr LEVEL "200" ->
-          let (li,id) = match fx with
+      | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
+          let fixp = mk_single_fix fx in
+          let (li,id) = match fixp with
               CFix(_,id,_) -> id
             | CCoFix(_,id,_) -> id
             | _ -> assert false in
-          CLetIn(loc,(li,Name id),fx,c)
+          CLetIn(loc,(li,Name id),fixp,c)
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
 	  po = return_type;
 	  ":="; c1 = operconstr LEVEL "200"; "in";
@@ -227,13 +231,15 @@ GEXTEND Gram
       | "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
   ;
   fix_constr:
-    [ [ kw=fix_kw; dcl=fix_decl ->
-          let (_,n,_,_,_,_) = dcl in mk_fix(loc,kw,n,[dcl])
-      | kw=fix_kw; dcl1=fix_decl; "with"; dcls=LIST1 fix_decl SEP "with";
+    [ [ fx1=single_fix -> mk_single_fix fx1
+      | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";
         "for"; id=identref ->
           mk_fix(loc,kw,id,dcl1::dcls)
     ] ]
-    ;
+  ;
+  single_fix:
+    [ [ kw=fix_kw; dcl=fix_decl -> (loc,kw,dcl) ] ]
+  ;
   fix_kw:
     [ [ "fix" -> true
       | "cofix" -> false ] ]
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 5a1f13132..aaf31da53 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -94,9 +94,9 @@ GEXTEND Gram
           body = tactic_expr -> TacLetRecIn (rcl,body)
       | "let"; llc = LIST1 let_clause SEP "with"; "in";
           u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
-      | "match"; IDENT "context"; "with"; mrl = match_context_list; "end" ->
+      | "match"; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           TacMatchContext (false,mrl)
-      | "match"; IDENT "reverse"; IDENT "context"; "with";
+      | "match"; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
           TacMatchContext (true,mrl)
       |	"match"; c = tactic_expr; "with"; mrl = match_list; "end" ->
@@ -114,15 +114,9 @@ GEXTEND Gram
       | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ];
 	  s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
       | st = simple_tactic -> TacAtom (loc,st)
-      | IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
-	  TacArg(ConstrMayEval (ConstrEval (rtc,c)))
-      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
-	  TacArg(ConstrMayEval (ConstrContext (id,c)))
-      | IDENT "check"; c = Constr.constr ->
-	  TacArg(ConstrMayEval (ConstrTypeOf c))
-      | IDENT "fresh"; s = OPT STRING ->
-	  TacArg (TacFreshId s)
-      | "'"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c))
+      | a = may_eval_arg -> TacArg(a)
+      | IDENT"constr"; ":"; c = Constr.constr ->
+          TacArg(ConstrMayEval(ConstrTerm c))
       | r = reference; la = LIST1 tactic_arg ->
           TacArg(TacCall (loc,r,la))
       | r = reference -> TacArg (Reference r) ]
@@ -132,10 +126,21 @@ GEXTEND Gram
   ;
   (* Tactic arguments *)
   tactic_arg:
-    [ [ "'"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+    [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+      | a = may_eval_arg -> a
       | a = tactic_atom -> a
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
   ;
+  may_eval_arg:
+    [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
+	  ConstrMayEval (ConstrEval (rtc,c))
+      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
+	  ConstrMayEval (ConstrContext (id,c))
+      | IDENT "type"; "of"; c = Constr.constr ->
+	  ConstrMayEval (ConstrTypeOf c)
+      | IDENT "fresh"; s = OPT STRING ->
+	  TacFreshId s ] ]
+  ;
   tactic_atom:
     [ [ id = METAIDENT -> MetaIdArg (loc,id)
       | r = reference -> Reference r
@@ -149,13 +154,7 @@ GEXTEND Gram
     [ [ id = identref; ":="; te = tactic_expr ->
           LETCLAUSE (id, None, arg_of_expr te)
       | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
-          LETCLAUSE (id, None, arg_of_expr (TacFun(args,te)))
-      | (_,id) = identref; ":"; c = Constr.lconstr; ":="; IDENT "proof" ->
-          LETTOPCLAUSE (id, c)
-      | id = identref; ":"; c = tactic_expr; ":="; te = tactic_expr ->
-          LETCLAUSE (id, Some c, arg_of_expr te)
-      |	(_,id) = identref; ":"; c = Constr.constr ->
-	  LETTOPCLAUSE (id, c) ] ]
+          LETCLAUSE (id, None, arg_of_expr (TacFun(args,te))) ] ]
   ;
   rec_clause:
     [ [ name = identref; it = LIST1 input_fun; ":="; body = tactic_expr ->
@@ -173,6 +172,8 @@ GEXTEND Gram
   match_context_rule:
     [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
         "=>"; te = tactic_expr -> Pat (largs, mp, te)
+      | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
+        "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te)
       | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
   match_context_list:
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 29dc5cfba..54af7a4f2 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -127,7 +127,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 if not !Options.v7 then
 GEXTEND Gram
-  GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
+  GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
     red_expr int_or_var castedopenconstr;
 
   int_or_var:
@@ -163,14 +163,6 @@ GEXTEND Gram
       |	id = METAIDENT -> MetaId (loc,id)
       ] ]
   ;
-  constrarg:
-    [ [ IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" ->
-        ConstrContext (id, c)
-      | IDENT "eval"; rtc = Tactic.red_expr; "in"; c = Constr.constr ->
-        ConstrEval (rtc,c) 
-      | IDENT "check"; c = Constr.constr -> ConstrTypeOf c
-      | c = Constr.constr -> ConstrTerm c ] ]
-  ;
   castedopenconstr:
     [ [ c = constr -> c ] ]
   ;
@@ -186,11 +178,16 @@ GEXTEND Gram
   conversion:
     [ [ c = constr -> (None, c)
       | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
-      | c1 = constr; IDENT "at"; nl = LIST1 integer; "with"; c2 = constr ->
+      | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr ->
 	  (Some (nl,c1), c2) ] ]
   ;
   pattern_occ:
-    [ [ c = constr; nl = LIST0 integer -> (nl,c) ] ]
+    [ [ c = constr; "at"; nl = LIST0 integer -> (nl,c)
+      | c = constr -> ([],c) ] ]
+  ;
+  unfold_occ:
+    [ [ c = global; "at"; nl = LIST0 integer -> (nl,c)
+      | c = global -> ([],c) ] ]
   ;
   pattern_occ_hyp_tail_list:
     [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ]
@@ -231,9 +228,6 @@ GEXTEND Gram
   with_binding_list:
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
-  unfold_occ:
-    [ [ c = global; nl = LIST0 integer -> (nl,c) ] ]
-  ;
   red_flag:
     [ [ IDENT "beta" -> FBeta
       | IDENT "delta" -> FDeltaBut []
@@ -252,7 +246,7 @@ GEXTEND Gram
       | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ SEP "," -> Pattern pl ] ]
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP","-> Pattern pl ] ]
   ;
   (* This is [red_tactic] including possible extensions *)
   red_expr:
@@ -394,8 +388,8 @@ GEXTEND Gram
       | IDENT "left"; bl = with_binding_list -> TacLeft bl
       | IDENT "right"; bl = with_binding_list -> TacRight bl
       | IDENT "split"; bl = with_binding_list -> TacSplit (false,bl)
-      | IDENT "exists"; bl = binding_list -> TacSplit (true,bl)
-      | IDENT "exists" -> TacSplit (true,NoBindings)
+      | "exists"; bl = binding_list -> TacSplit (true,bl)
+      | "exists" -> TacSplit (true,NoBindings)
       | IDENT "constructor"; n = num_or_meta; l = with_binding_list ->
 	  TacConstructor (n,l)
       | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor t
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 05aea1015..91e765dc4 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -28,7 +28,7 @@ open Vernac_
 open Module
 
 
-let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..."; "where" ]
+let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..."; "where"; "at" ]
 let _ = 
   if not !Options.v7 then
     List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
@@ -337,8 +337,7 @@ GEXTEND Gram
   export_token:
     [ [ IDENT "Import" -> Some false
       | IDENT "Export" -> Some true
-      | IDENT "Closed" -> None
-      |  -> Some false ] ]
+      |  -> None ] ]
   ;
   specif_token:
     [ [ IDENT "Implementation" -> Some false
@@ -723,10 +722,10 @@ GEXTEND Gram
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
   ;
   syntax_modifier:
-    [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev)
-      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; 
+    [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; 
         lev = level -> SetItemLevel (x::l,lev)
-      | IDENT "at"; IDENT "level"; n = natural -> SetLevel n
+      | "at"; IDENT "level"; n = natural -> SetLevel n
       | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index a77b03223..0ee86be93 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,7 +50,7 @@ val w_conv_x            : wc -> constr -> constr -> bool
 val w_const_value       : wc -> constant -> constr
 val w_defined_evar      : wc -> existential_key -> bool
 
-val instantiate : int -> constr -> Tacticals.clause -> tactic
+val instantiate : int -> constr -> identifier option -> tactic
 (*
 val instantiate_tac : tactic_arg list -> tactic
 *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 276e033ac..152b80e2a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -113,12 +113,18 @@ END
 (* AutoRewrite *)
 
 open Autorewrite
-TACTIC EXTEND Autorewrite
+TACTIC EXTEND AutorewriteV7
   [ "AutoRewrite" "[" ne_preident_list(l) "]" ] ->
     [ autorewrite Refiner.tclIDTAC l ]
 | [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] ->
     [ autorewrite (snd t) l ]
 END
+TACTIC EXTEND AutorewriteV8
+  [ "AutoRewrite" "with" ne_preident_list(l) ] ->
+    [ autorewrite Refiner.tclIDTAC l ]
+| [ "AutoRewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
+    [ autorewrite (snd t) l ]
+END
 
 let add_rewrite_hint name ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
@@ -126,7 +132,7 @@ let add_rewrite_hint name ort t lcsr =
   add_rew_rules name (List.map f lcsr)
 
 (* V7 *)
-VERNAC COMMAND EXTEND HintRewrite_v7
+VERNAC COMMAND EXTEND HintRewriteV7
   [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] ->
   [ add_rewrite_hint b o Tacexpr.TacId l ]
 | [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b)
@@ -135,7 +141,7 @@ VERNAC COMMAND EXTEND HintRewrite_v7
 END
 
 (* V8 *)
-VERNAC COMMAND EXTEND HintRewrite
+VERNAC COMMAND EXTEND HintRewriteV8
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
   [ add_rewrite_hint b o Tacexpr.TacId l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0c0a0f592..001e762d1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -472,12 +472,8 @@ let apply_without_reduce c gl =
   let clause = mk_clenv_type_of wc c in 
   res_pf kONT clause gl
 
-(* Dead code
-let refinew_scheme kONT clause gl = res_pf kONT clause gl
-*)
-
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
-   |- B -> C and |- A (which is realized by Cut B;[Idtac|Apply c]
+   |- B -> C and |- A
 
    -------------------
    Gamma |- c : A -> B      Gamma |- ?2 : A
@@ -485,7 +481,13 @@ let refinew_scheme kONT clause gl = res_pf kONT clause gl
            Gamma |- B                        Gamma |- ?1 : B -> C
            -----------------------------------------------------
                              Gamma |- ? : C
- *)
+
+ Ltac lapply c :=
+  let ty := check c in
+  match eval hnf in ty with
+    ?A -> ?B => cut B; [ idtac | apply c ]
+  end.
+*)
 
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index c9a5c2cc0..4919dddac 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -54,7 +54,7 @@ let is_disj ist =
 
 let not_dep_intros ist =
   <:tactic<
-  repeat match context with
+  repeat match goal with
   | |- (?X1 -> ?X2) => intro
   | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff
   | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not
@@ -68,7 +68,7 @@ let axioms ist =
   let t_is_unit = tacticIn is_unit
   and t_is_empty = tacticIn is_empty in
     <:tactic<
-    match reverse context with
+    match reverse goal with
       | |- ?X1 => $t_is_unit; constructor 1
       | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
       | _:?X1 |- ?X1 => assumption
@@ -83,7 +83,7 @@ let simplif ist =
   <:tactic<
     $t_not_dep_intros;
     repeat
-       (match reverse context with
+       (match reverse goal with
         | id: (?X1 _ _) |- _ =>
             $t_is_conj; elim id; do 2 intro; clear id
         | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id
@@ -127,7 +127,7 @@ let rec tauto_intuit t_reduce solver ist =
   let t_solver = Tacexpr.TacArg (valueIn (VTactic (dummy_loc,solver))) in
   <:tactic<
    ($t_simplif;$t_axioms
-   || match reverse context with
+   || match reverse goal with
       | id:(?X1-> ?X2)-> ?X3|- _ =>
 	  cut X3;
 	    [ intro; clear id; $t_tauto_intuit 
@@ -140,7 +140,7 @@ let rec tauto_intuit t_reduce solver ist =
       end
     ||
     (* NB: [|- _ -> _] matches any product *)
-    match context with | |- _ -> _ => intro; $t_tauto_intuit
+    match goal with | |- _ -> _ => intro; $t_tauto_intuit
     |  |- _  => $t_reduce;$t_solver
     end
     ||
@@ -149,7 +149,7 @@ let rec tauto_intuit t_reduce solver ist =
     
 let reduction_not_iff=interp
  <:tactic<repeat 
-  match context with 
+  match goal with 
   | |- _     => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff 
   | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
   end >>
@@ -173,7 +173,7 @@ let default_intuition_tac = interp <:tactic< auto with * >>
 
 let q_elim tac=
   <:tactic<
-  match context with 
+  match goal with 
     x : ?X1, H : ?X1 -> _ |- _ => generalize (H x); clear H; $tac
   end >>
 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index e2fa1d88f..f98a160c4 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -18,7 +18,7 @@ Uninterpreted Notation "x \/ y" (at level 7, right associativity)
   V8only (at level 85, right associativity).
 
 Uninterpreted Notation "x <-> y" (at level 8, right associativity)
-  V8only (at level 90, right associativity).
+  V8only (at level 95, no associativity).
 
 Uninterpreted Notation "~ x" (at level 5, right associativity)
   V8only (at level 75, right associativity).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cdb9574e6..5fe640cc5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -542,15 +542,27 @@ let make_anon_notation symbols =
 let make_symbolic n symbols etyps =
   ((n,List.map (assoc_of_type n) etyps), make_anon_notation symbols)
 
+let is_not_small_constr = function
+    ETConstr _ -> true
+  | ETOther("constr","binder_constr") -> true
+  | _ -> false
+
 let rec define_keywords = function
-    NonTerm(_,Some(_,(ETConstr _|ETOther("constr","binder_constr")))) as n1 ::
-    Term("IDENT",k) :: l when not !Options.v7 ->
+    NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l
+     when not !Options.v7 && is_not_small_constr e ->
       prerr_endline ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
       n1 :: Term("",k) :: define_keywords l
   | n :: l -> n :: define_keywords l
   | [] -> []
 
+let define_keywords = function
+    Term("IDENT",k)::l when not !Options.v7 ->
+      prerr_endline ("Defining '"^k^"' as keyword");
+      Lexer.add_token("",k);
+      Term("",k) :: define_keywords l
+  | l -> define_keywords l
+
 let make_production etyps symbols =
   let prod =
     List.fold_right
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 6177f1a96..0154110e5 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -418,7 +418,7 @@ let rec pr inherited a =
 	str"fun" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
         str " =>" ++ spc() ++ pr ltop a),
       llambda
-  | CLetIn (_,(_,Name x),(CFix(_,(_,x'),_)|CCoFix(_,(_,x'),_) as fx), b)
+  | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
       when x=x' ->
       hv 0 (
         hov 2 (str "let " ++ pr ltop fx ++ str " in") ++
@@ -600,8 +600,15 @@ let pr_lrawconstr_env env c =
 
 let pr_cases_pattern = pr_patt ltop
 
-let pr_occurrences prc (nl,c) =
-   prc c ++ prlist (fun n -> spc () ++ int n) nl
+let pr_pattern_occ prc = function
+    ([],c) -> prc c
+  | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++
+                     hov 0 (prlist_with_sep spc int nl))
+
+let pr_unfold_occ pr_ref = function
+    ([],qid) -> pr_ref qid
+  | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++
+                       hov 0 (prlist_with_sep spc int nl))
 
 let pr_qualid qid = str (string_of_qualid qid)
 
@@ -627,7 +634,7 @@ let pr_metaid id = str"?" ++ pr_id id
 let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Red false -> str "red"
   | Hnf -> str "hnf"
-  | Simpl o -> str "simpl" ++ pr_opt (pr_occurrences pr_constr) o  
+  | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) o  
   | Cbv f ->
       if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
 	str "compute"
@@ -636,13 +643,12 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Lazy f -> 
       hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
   | Unfold l ->
-      hov 1 (str "unfold " ++
-        prlist_with_sep pr_coma (fun (nl,qid) ->
-	  pr_ref qid ++ prlist (pr_arg int) nl) l)
+      hov 1 (str "unfold" ++ spc() ++
+             prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l)
   | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l ->
       hov 1 (str "pattern" ++
-        pr_arg (prlist_with_sep pr_coma (pr_occurrences pr_constr)) l)
+        pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l)
         
   | Red true -> error "Shouldn't be accessible from user"
   | ExtraRedExpr (s,c) ->
@@ -656,10 +662,10 @@ let rec pr_may_eval prc prlc pr2 = function
 	 str " in" ++ spc() ++ prc c)
   | ConstrContext ((_,id),c) ->
       hov 0
-	(str "inst " ++ pr_id id ++ spc () ++
+	(str "context " ++ pr_id id ++ spc () ++
 	 str "[" ++ prlc c ++ str "]")
-  | ConstrTypeOf c -> hov 1 (str "check" ++ spc() ++ prc c)
-  | ConstrTerm c -> prlc c
+  | ConstrTypeOf c -> hov 1 (str "type of" ++ spc() ++ prc c)
+  | ConstrTerm c -> prc c
 
 let pr_rawconstr_env_no_translate env c =
   pr lsimple (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 565da88ca..7b9ba49d8 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -265,7 +265,7 @@ let pr_match_rule m pr pr_pat = function
   | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
 let pr_funvar = function
-  | None -> spc () ++ str "()"
+  | None -> spc () ++ str "_"
   | Some id -> spc () ++ pr_id id
 
 let pr_let_clause k pr = function
@@ -305,15 +305,15 @@ let pr_hintbases = function
 let pr_autoarg_adding = function
   | [] -> mt ()
   | l ->
-      spc () ++ str "Adding [" ++
+      spc () ++ str "adding [" ++
         hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
 
 let pr_autoarg_destructing = function
-  | true -> spc () ++ str "Destructing"
+  | true -> spc () ++ str "destructing"
   | false -> mt ()
 
 let pr_autoarg_usingTDB = function
-  | true -> spc () ++ str "Using TDB"
+  | true -> spc () ++ str "using tdb"
   | false -> mt ()
 
 let rec pr_tacarg_using_rule pr_gen = function
@@ -555,17 +555,16 @@ and pr_atom1 env = function
   | TacReduce (r,h) ->
       hov 1 (pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) r ++
              pr_clause pr_ident h)
-  | TacChange (occ,c,h) -> (* A Verifier *)
+  | TacChange (occ,c,h) ->
       hov 1 (str "change" ++ brk (1,1) ++
       (match occ with
           None -> mt()
+        | Some([],c1) ->
+            hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
         | Some(ocl,c1) ->
             hov 1 (pr_constr env c1 ++ spc() ++
-	    if ocl <> [] then
-	      str "at " ++ prlist (fun i -> int i ++ spc()) ocl
-	    else
-	      mt ()) ++
-	    spc() ++ str "with ") ++
+	           str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+	           str "with ") ++
       pr_constr env c ++ pr_clause pr_ident h)
 
   (* Equivalence relations *)
@@ -632,7 +631,7 @@ let rec pr_tac env inherited tac =
       lmatch
   | TacMatchContext (lr,lrul) ->
       hov 0 (
-	str (if lr then "match reverse context with" else "match context with")
+	str (if lr then "match reverse goal with" else "match goal with")
 	++ prlist
 	  (fun r -> fnl () ++ str "| " ++
             pr_match_rule false (pr_tac env ltop) pr_pat r)
@@ -683,9 +682,11 @@ let rec pr_tac env inherited tac =
   | TacAtom (loc,t) ->
       pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
   | TacArg(Tacexp e) -> pr_tac0 env e, latom
-  | TacArg(ConstrMayEval (ConstrTerm c)) -> str "'" ++ pr_constr env c, latom
+  | TacArg(ConstrMayEval (ConstrTerm c)) ->
+      str "constr:" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
+  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qsnew sopt, latom
   | TacArg(Integer n) -> int n, latom
   | TacArg(TacCall(loc,f,l)) ->
       pr_with_comments loc
@@ -704,10 +705,11 @@ and pr_tacarg env = function
   | Identifier id -> pr_id id
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
-  | ConstrMayEval (ConstrTerm c) -> pr_constr env c
+  | ConstrMayEval c ->
+      pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c
   | TacFreshId sopt -> str "fresh" ++ pr_opt qsnew sopt
-  | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a ->
-      str "'" ++ pr_tac env (latom,E) (TacArg a)
+  | (TacCall _|Tacexp _|Integer _) as a ->
+      str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
 
 in ((fun env -> pr_tac env ltop),
     (fun env -> pr_tac env (latom,E)),
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index e2a4d22e4..2a8cc3c9b 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -370,9 +370,9 @@ let pr_thm_token = function
   | Remark -> str"Remark"
 
 let pr_require_token = function
-  | Some true -> str "Export"
-  | Some false -> str "Import"
-  | None -> str "Closed"
+  | Some true -> str " Export"
+  | Some false -> str " Import"
+  | None -> mt()
 
 let pr_syntax_modifier = function
   | SetItemLevel (l,NextLevel) ->
@@ -718,7 +718,7 @@ let rec pr_vernac = function
           str key ++ spc() ++
           pr_id id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
 	  spc() ++ pr_type s ++ 
-	  str" :=") ++ pr_constructor_list lc ++ fnl () ++ 
+	  str" :=") ++ pr_constructor_list lc ++ 
 	pr_decl_notation pr_constr ntn in
 
       (* Copie simplifiée de command.ml pour déclarer les notations locales *)
@@ -833,7 +833,7 @@ let rec pr_vernac = function
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_id id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_id id)
   | VernacRequire (exp,spe,l) -> hov 2
-      (str "Require " ++ pr_require_token exp ++ spc() ++
+      (str "Require" ++ pr_require_token exp ++ spc() ++
       (match spe with
       |	None -> mt()
       |	Some flag ->