nouvelle syntaxe de ltac

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

14 files changed, 175 insertions, 176 deletions

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 437fb0fff..87a9033f6 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 context 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/interface/ascent.mli b/contrib/interface/ascent.mli
index 428606be7..84c07dc71 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -338,7 +338,7 @@ and ct_IN_OR_OUT_MODULES =
   | CT_in_modules of ct_ID_NE_LIST
   | CT_out_modules of ct_ID_NE_LIST
 and ct_LET_CLAUSE =
-    CT_let_clause of ct_ID * ct_DEF_BODY_OPT * ct_LET_VALUE
+    CT_let_clause of ct_ID * ct_TACTIC_OPT * ct_LET_VALUE
 and ct_LET_CLAUSES =
     CT_let_clauses of ct_LET_CLAUSE * ct_LET_CLAUSE list
 and ct_LET_VALUE =
@@ -524,7 +524,7 @@ and ct_TACTIC_COM =
   | CT_lettac of ct_ID * ct_FORMULA * ct_UNFOLD_LIST
   | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
-  | CT_match_tac of ct_LET_VALUE * ct_MATCH_TAC_RULES
+  | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
   | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST
   | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index df83a0499..677f7edc9 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -795,7 +795,7 @@ and fIN_OR_OUT_MODULES = function
 and fLET_CLAUSE = function
 | CT_let_clause(x1, x2, x3) ->
    fID x1;
-   fDEF_BODY_OPT x2;
+   fTACTIC_OPT x2;
    fLET_VALUE x3;
    fNODE "let_clause" 3
 and fLET_CLAUSES = function
@@ -1243,7 +1243,7 @@ and fTACTIC_COM = function
    (List.iter fCONTEXT_RULE l);
    fNODE "match_context_reverse" (1 + (List.length l))
 | CT_match_tac(x1, x2) ->
-   fLET_VALUE x1;
+   fTACTIC_COM x1;
    fMATCH_TAC_RULES x2;
    fNODE "match_tac" 2
 | CT_move_after(x1, x2) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 02300fdfd..6fd12a010 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -710,7 +710,7 @@ and xlate_tactic =
    | TacProgress t -> CT_progress(xlate_tactic t)
    | TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2)
    | TacMatch (exp, rules) ->
-        CT_match_tac(CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body exp),
+        CT_match_tac(xlate_tactic exp,
                      match List.map 
                        (function 
                           | Pat ([],p,tac) ->
@@ -737,23 +737,22 @@ and xlate_tactic =
          function
              ((_,s),None,ConstrMayEval v) ->
                  CT_let_clause(xlate_ident s,
-			       ctv_DEF_BODY_OPT_NONE,
+			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_DEF_BODY_to_LET_VALUE
                                (formula_to_def_body v))
            | ((_,s),None,Tacexp t) -> 
                  CT_let_clause(xlate_ident s,
-			       ctv_DEF_BODY_OPT_NONE,
+			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
                                (xlate_tactic t))
            | ((_,s),None,t) -> 
                  CT_let_clause(xlate_ident s,
-			       ctv_DEF_BODY_OPT_NONE,
+			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
                                (xlate_call_or_tacarg t))
            | ((_,s),Some c,t) -> 
 	       CT_let_clause(xlate_ident s,
-			     CT_coerce_DEF_BODY_to_DEF_BODY_OPT
-			     (formula_to_def_body c),
+			     CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic c),
                                CT_coerce_TACTIC_COM_to_LET_VALUE
 				 (xlate_call_or_tacarg t)) in
          let cl_l = List.map cvt_clause l in
@@ -761,7 +760,6 @@ and xlate_tactic =
             | [] -> assert false 
             | fst::others ->
                 CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t))
-   | TacLetCut _ -> xlate_error "Unclear future of syntax Let x := t"
    | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition"
    | TacLetRecIn(f1::l, t) -> 
        let tl =  CT_rec_tactic_fun_list
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index ccb5c1077..41e5eb62a 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -17,6 +17,7 @@
 
 \def\bfbar{\ensuremath{|\hskip -0.22em{}|\hskip -0.24em{}|}}
 \def\TERMbar{\bfbar}
+\def\TERMbarbar{\bfbar\bfbar}
 \def\notv{\text{_}}
 \def\infx#1{\notv#1\notv}
 
@@ -360,11 +361,26 @@ $$
 
 \section{Grammar of tactics}
 
-\subsection{Basic tactics}
-
 \def\tacconstr{\NTL{constr}{9}}
 \def\taclconstr{\NTL{constr}{200}}
 
+Additional symbols are:
+$$ \TERM{'}
+~~ \KWD{;}
+~~ \TERM{()}
+~~ \TERMbarbar
+~~ \TERM{$\vdash$}
+~~ \TERM{[}
+~~ \TERM{]}
+~~ \TERM{$\leftarrow$}
+$$
+Additional reserved keywords are:
+$$ \KWD{at}
+~~ \TERM{using}
+$$
+
+\subsection{Basic tactics}
+
 \begin{rules}
 \DEFNT{simple-tactic}
        \TERM{intros}~\TERM{until}~\NT{quantified-hyp}
@@ -444,6 +460,11 @@ $$
 \nlsep \TERM{symmetry}
 \nlsep \TERM{transitivity}~\tacconstr
 %%
+\nlsep \NT{inversion-kwd}~\NT{quantified-hyp}~\NT{with-names}~\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 \NT{red-expr}~\NT{clause}
 \nlsep \TERM{change}~\NT{conversion}~\NT{clause}
 \SEPDEF
@@ -458,8 +479,12 @@ $$
 \SEPDEF
 \DEFNT{conversion}
        \tacconstr~\TERM{at}~\PLUS{\NT{int}}~\KWD{with}~\tacconstr
-       \tacconstr~\KWD{with}~\tacconstr
+\nlsep \tacconstr~\KWD{with}~\tacconstr
 \nlsep \tacconstr
+\SEPDEF
+\DEFNT{inversion-kwd}
+       \TERM{inversion} ~\mid~ \TERM{invesion_clear} ~\mid~
+       \TERM{simple}~\TERM{inversion}
 \end{rules}
 
 Conflicts exists between integers and constrs.
@@ -471,7 +496,6 @@ Conflicts exists between integers and constrs.
 \DEFNT{induction-arg}
        \NT{int}~\mid~\tacconstr
 \SEPDEF
-%% TODO: lconstr not followed by a keyword
 \DEFNT{fix-spec}
        \KWD{(}~\NT{ident}~\STAR{\NT{binder}}~\OPT{\NT{annot}}
        ~\KWD{:}~\taclconstr~\KWD{)}
@@ -505,13 +529,15 @@ Conflicts exists between integers and constrs.
 \nlsep \PLUS{\NT{simple-binding}}
 \SEPDEF
 \DEFNT{simple-binding}
-       \KWD{(}~\NT{quantified-hyp}~\KWD{:=}~\NT{constr}~\KWD{)}
+       \KWD{(}~\NT{quantified-hyp}~\KWD{:=}~\taclconstr~\KWD{)}
 \SEPDEF
 \DEFNT{pattern-occ}
-       \tacconstr~\STAR{\NT{int}}
+       \KWD{(} ~\NT{constr} ~\OPTGR{\KWD{at}~\PLUS{\NT{int}}} ~\KWD{)}
+\nlsep \tacconstr
 \SEPDEF
 \DEFNT{unfold-occ}
-       \NT{reference}~\STAR{\NT{int}}
+       \KWD{(} \NT{reference}~\OPTGR{\KWD{at}~\PLUS{\NT{int}}} ~\KWD{)}
+\nlsep \NT{reference}
 \SEPDEF
 \DEFNT{red-flag}
        \TERM{beta} ~\mid~ \TERM{iota} ~\mid~ \TERM{zeta}
@@ -519,7 +545,7 @@ Conflicts exists between integers and constrs.
        \TERM{delta}~\OPT{\TERM{-}}~\TERM{[}~\PLUS{\NT{reference}}~\TERM{]}
 \SEPDEF
 \DEFNT{clause}
-       \OPTGR{\KWD{in}~\NT{hyp-ident}}
+       \OPTGR{\KWD{in}~\PLUS{\NT{hyp-ident}}}
 \SEPDEF
 \DEFNT{hyp-ident}
        \NT{ident}
@@ -543,17 +569,6 @@ Conflicts exists between integers and constrs.
 
 \subsection{Ltac}
 
-Additional symbols are:
-$$ \TERM{'}
-~~ \KWD{;}
-~~ \TERM{()}
-~~ \TERM{$\vdash$}
-$$
-Additional reserved keywords are:
-$$ \TERM{orelse}
-~~ \TERM{using}
-$$
-
 Currently, there are conflicts with keyword \KWD{in}: in the following,
 has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \begin{center}
@@ -573,15 +588,15 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \nlsep \TERM{progress} ~\NT{tactic}
 \nlsep \TERM{info} ~\NT{tactic}
 %%
-\nlsep \NT{tactic} ~\TERM{orelse} ~\NT{tactic} &2R &\RNAME{Orelse}
+\nlsep \NT{tactic} ~\TERMbarbar ~\NT{tactic} &2R &\RNAME{Orelse}
 %%
 \nlsep \KWD{fun} ~\PLUS{\NT{name}} ~\KWD{$\Rightarrow$}
        ~\NT{tactic}  &1 &\RNAME{Fun-tac}
-\nlsep \TERM{rec} ~\NT{rec-clauses} ~\KWD{in} ~\NT{tactic}
 \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} ~\NTL{constr}{100} ~\KWD{with}
+\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}}
 \nlsep \TERM{first}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
@@ -589,8 +604,8 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \nlsep \TERM{idtac}
 \nlsep \TERM{fail} ~\OPT{\NT{int}} ~\OPT{\NT{string}}
 \nlsep \TERM{fresh} ~\OPT{\NT{string}}
-\nlsep \TERM{context} ~\NT{ident} ~\TERM{[} ~\NT{constr} ~\TERM{]}
-\nlsep \TERM{eval} ~\NT{red-expr} ~\KWD{in} ~\NT{constr}
+\nlsep \TERM{context} ~\NT{ident} ~\TERM{[} ~\taclconstr ~\TERM{]}
+\nlsep \TERM{eval} ~\NT{red-expr} ~\KWD{in} ~\tacconstr
 \nlsep \TERM{check} ~\tacconstr
 \nlsep \TERM{'} ~\tacconstr
 \nlsep \NT{reference}~\STAR{\NT{tactic-arg}}  &&\RNAME{call-tactic}
@@ -606,7 +621,6 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \SEPDEF
 \DEFNT{tactic-atom}
        \NT{reference}
-\nlsep \NT{meta-ident}
 \nlsep \TERM{()}
 \SEPDEF
 \DEFNT{tactic-seq}
@@ -621,8 +635,10 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
        \NT{let-clause} ~\STARGR{\KWD{with}~\NT{let-clause}}
 \SEPDEF
 \DEFNT{let-clause}
-       \NT{ident} ~\STAR{\NT{name}} ~\NT{type-cstr} ~\KWD{:=} ~\NT{tactic}
-\nlsep \NT{ident} ~\KWD{:} ~\NT{constr} ~\OPTGR{\KWD{:=}~\TERM{proof}}
+       \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}
@@ -638,6 +654,7 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \DEFNT{match-ctxt-rule}
        \NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
        ~\KWD{$\Rightarrow$} ~\NT{tactic}
+\nlsep \KWD{_} ~\KWD{$\Rightarrow$} ~\NT{tactic}
 \SEPDEF
 \DEFNT{match-hyps-list}
        \NT{match-hyps} ~\KWD{,} ~\NT{match-hyps-list}
@@ -652,6 +669,7 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \SEPDEF
 \DEFNT{match-rule}
        \NT{match-pattern} ~\KWD{$\Rightarrow$} ~\NT{tactic}
+\nlsep \KWD{_} ~\KWD{$\Rightarrow$} ~\NT{tactic}
 \SEPDEF
 \DEFNT{match-pattern}
        \TERM{context}~\OPT{\NT{ident}}
@@ -662,11 +680,56 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
        \tacconstr
 \end{rules}
 
+\subsection{Other tactics}
+
+TODO
+
+\begin{rules}
+\EXTNT{simple-tactic}
+       \TERM{rewrite}
+\nlsep \TERM{replace}
+\nlsep \TERM{symplify_eq}
+\nlsep \TERM{discriminate}
+\nlsep \TERM{injection}
+\nlsep \TERM{conditional rewrite}
+\nlsep \TERM{dependent rewrite}
+\nlsep \TERM{absurd}
+\nlsep \TERM{contradiction}
+\nlsep \TERM{autorewrite}
+\nlsep \TERM{hint rewrite}
+\nlsep \TERM{refine}
+\nlsep \TERM{setoid_replace}
+\nlsep \TERM{setoid_rewrite}
+\nlsep \TERM{add setoid}
+\nlsep \TERM{add morphism}
+\nlsep \TERM{inversion}
+\nlsep \TERM{simple}~\TERM{inversion}
+\nlsep \TERM{derive}~\TERM{inversion_clear}
+\nlsep \TERM{derive}~\TERM{inversion}
+\nlsep \TERM{derive}~\TERM{dependent}~\TERM{inversion}
+\nlsep \TERM{derive}~\TERM{dependent}~\TERM{inversion_clear}
+\nlsep \TERM{subst}
+%% eqdecide.ml4
+\nlsep \TERM{decide}~\TERM{equality}
+\nlsep \TERM{compare}
+%% eauto
+\nlsep \TERM{eexact}
+\nlsep \TERM{eapply}
+\nlsep \TERM{prolog}
+\nlsep \TERM{eauto}
+\nlsep \TERM{eautod}
+%% tauto
+\nlsep \TERM{tauto}
+\nlsep \TERM{simplif}
+\nlsep \TERM{intuition}
+\nlsep \TERM{linearintuition}
+\end{rules}
+
 \section{Grammar of commands}
 
 New symbols:
 $$ \TERM{.}
-~~ \TERM{!!}
+~~ \TERM{..}
 ~~ \TERM{\tt >->}
 ~~ \TERM{:$>$}
 ~~ \TERM{$<$:}
@@ -688,7 +751,7 @@ $$
 \DEFNT{subgoal-command}
        \NT{check-command}
 \nlsep %\OPT{\TERM{By}}~
-   \OPT{\TERM{!!}}~\NT{tactic}
+   \NT{tactic}~\OPT{\KWD{..}}
 \end{rules}
 
 \subsection{Gallina and extensions}
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b342d9716..41ee54ea4 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -31,7 +31,7 @@ open Q
 type let_clause_kind =
   | LETTOPCLAUSE of Names.identifier * constr_expr
   | LETCLAUSE of
-      (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg)
+      (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
 
 ifdef Quotify then
 module Prelude = struct
@@ -82,7 +82,7 @@ GEXTEND Gram
       | id = base_ident; ":"; c = Constr.constr; ":="; "Proof" ->
           LETTOPCLAUSE (id, c)
       | id = identref; ":"; c = constrarg; ":="; te = tactic_letarg ->
-          LETCLAUSE (id, Some c, te)
+          LETCLAUSE (id, Some (TacArg(ConstrMayEval c)), te)
       |	id = base_ident; ":"; c = Constr.constr ->
 	  LETTOPCLAUSE (id, c) ] ]
   ;
@@ -150,35 +150,13 @@ GEXTEND Gram
 	  [IDENT "In" | "in"]; body = tactic_expr -> TacLetRecIn (rc::rcl,body)
       | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In";
           u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
-(* Let cas LetCut est subsumé par "Assert id := c" tandis que le cas
-   StartProof ne fait pas vraiment de sens en tant que sous-expression
-   d'une tactique complexe... 
-      |	IDENT "Let"; llc = LIST1 let_clause SEP "And" -> 
-        (match llc with
-	| [LETTOPCLAUSE (id,c)] ->
-	    VernacStartProof ((NeverDischarge,false),id,c,true,(fun _ _ -> ()))
-        | l ->
-	    let l = List.map (function
-	      | LETCLAUSE (id,Some a,t) -> (id,a,t)
-	      | _ -> user_err_loc (loc, "", str "Syntax Error")) l in
-	    TacLetCut (loc, l))
-*)
-(*
-      |	IDENT "Let"; llc = LIST1 let_clause SEP "And";
-        tb = Vernac_.theorem_body; "Qed" ->
-          (match llc with
-	    | [LETTOPCLAUSE (id,c)] ->
-		EscapeVernac <:ast< (TheoremProof "LETTOP" $id $c $tb) >>
-	    | _ ->
-		errorlabstrm "Gram.tactic_atom" (str "Not a LETTOPCLAUSE"))
-*)
 
       | IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
         -> TacMatchContext (false,mrl)
       | IDENT "Match"; IDENT "Reverse"; IDENT "Context"; IDENT "With"; mrl = match_context_list
         -> TacMatchContext (true,mrl)
       |	IDENT "Match"; c = constrarg; IDENT "With"; mrl = match_list ->
-        TacMatch (c,mrl)
+        TacMatch (TacArg(ConstrMayEval c),mrl)
 (*To do: put Abstract in Refiner*)
       | IDENT "Abstract"; tc = tactic_expr -> TacAbstract (tc,None)
       | IDENT "Abstract"; tc = tactic_expr; "using";  s = base_ident ->
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 9d8dea149..5a1f13132 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -31,7 +31,7 @@ open Q
 type let_clause_kind =
   | LETTOPCLAUSE of Names.identifier * constr_expr
   | LETCLAUSE of
-      (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg)
+      (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
 
 ifdef Quotify then
 module Prelude = struct
@@ -99,7 +99,7 @@ GEXTEND Gram
       | "match"; IDENT "reverse"; IDENT "context"; "with";
         mrl = match_context_list; "end" ->
           TacMatchContext (true,mrl)
-      |	"match"; c = constrarg; "with"; mrl = match_list; "end" ->
+      |	"match"; c = tactic_expr; "with"; mrl = match_list; "end" ->
           TacMatch (c,mrl)
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = tactic_expr -> TacAbstract (tc,None)
@@ -116,7 +116,7 @@ GEXTEND Gram
       | st = simple_tactic -> TacAtom (loc,st)
       | IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
 	  TacArg(ConstrMayEval (ConstrEval (rtc,c)))
-      | IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" ->
+      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
 	  TacArg(ConstrMayEval (ConstrContext (id,c)))
       | IDENT "check"; c = Constr.constr ->
 	  TacArg(ConstrMayEval (ConstrTypeOf c))
@@ -148,11 +148,13 @@ GEXTEND Gram
   let_clause:
     [ [ id = identref; ":="; te = tactic_expr ->
           LETCLAUSE (id, None, arg_of_expr te)
-      | (_,id) = identref; ":"; c = Constr.constr; ":="; IDENT "proof" ->
+      | 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 = constrarg; ":="; te = tactic_expr ->
+      | id = identref; ":"; c = tactic_expr; ":="; te = tactic_expr ->
           LETCLAUSE (id, Some c, arg_of_expr te)
-      |	(_,id) = identref; ":"; c = Constr.lconstr ->
+      |	(_,id) = identref; ":"; c = Constr.constr ->
 	  LETTOPCLAUSE (id, c) ] ]
   ;
   rec_clause:
@@ -160,16 +162,16 @@ GEXTEND Gram
           (name,(it,body)) ] ]
   ;
   match_pattern:
-    [ [ id = Constr.lconstr_pattern; "["; pc = Constr.lconstr_pattern; "]" ->
-        let s = coerce_to_id id in Subterm (Some s, pc)
-      | "["; pc = Constr.lconstr_pattern; "]" -> Subterm (None,pc)
+    [ [ IDENT "context";  oid = OPT Constr.ident;
+          "["; pc = Constr.lconstr_pattern; "]" ->
+        Subterm (oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
   match_hyps:
     [ [ na = name; ":"; mp =  match_pattern -> Hyp (na, mp) ] ]
   ;
   match_context_rule:
-    [ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]";
+    [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
         "=>"; te = tactic_expr -> Pat (largs, mp, te)
       | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
@@ -178,7 +180,7 @@ GEXTEND Gram
       | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
   ;
   match_rule:
-    [ [ "["; mp = match_pattern; "]"; "=>"; te = tactic_expr -> Pat ([],mp,te)
+    [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te)
       | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
   match_list:
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 0d7230453..968415de1 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -631,12 +631,8 @@ and pr6 = function
   | TacLetIn (llc,u) ->
       v 0
        (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "In") ++ fnl () ++ prtac u)
-  | TacLetCut llc ->
-      pr_let_clauses pr_tacarg0
-        (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc)
-      ++ fnl ()
   | TacMatch (t,lrul) ->
-      hov 0 (str "Match" ++ spc () ++ pr_may_eval pr_constr pr_cst t ++ spc()
+      hov 0 (str "Match" ++ spc () ++ pr6 t ++ spc()
         ++ str "With"
         ++ prlist
 	  (fun r -> fnl () ++ str "|" ++ spc () ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 44e78462f..7dd14d87a 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -481,15 +481,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       let f =
 	mlexpr_of_triple
 	  (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident)
-	  (mlexpr_of_option (mlexpr_of_may_eval mlexpr_of_constr))
+	  (mlexpr_of_option mlexpr_of_tactic)
 	  mlexpr_of_tactic_arg in
       <:expr< Tacexpr.TacLetIn $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
-(*
-  | Tacexpr.TacLetCut of (identifier * t * tactic_expr) list
-*)
   | Tacexpr.TacMatch (t,l) ->
       <:expr< Tacexpr.TacMatch
-        $mlexpr_of_may_eval mlexpr_of_constr t$
+        $mlexpr_of_tactic t$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
   | Tacexpr.TacMatchContext (lr,l) ->
       <:expr< Tacexpr.TacMatchContext 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 4435d57ab..062842e73 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -195,9 +195,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
 
   | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacLetIn of (identifier located * ('constr,'cst) may_eval option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacLetCut of (identifier * ('constr,'cst) may_eval * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list
-  | TacMatch of ('constr,'cst) may_eval * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacMatch of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
   | TacMatchContext of direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
   | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 460d0bc38..da5ab1772 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -689,17 +689,14 @@ and intern_tactic_seq ist = function
   | TacLetIn (l,u) ->
       let l = List.map
         (fun (n,c,b) ->
-          (n,option_app (intern_constr_may_eval ist) c, intern_tacarg !strict_check ist b)) l in
+          (n,option_app (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
       let (l1,l2) = ist.ltacvars in
       let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
       ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
-  | TacLetCut l ->
-      let f (n,c,t) = (n,intern_constr_may_eval ist c,intern_tacarg !strict_check ist t) in
-      ist.ltacvars, TacLetCut (List.map f l)
   | TacMatchContext (lr,lmr) ->
       ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr)
   | TacMatch (c,lmr) ->
-      ist.ltacvars, TacMatch (intern_constr_may_eval ist c,intern_match_rule ist lmr)
+      ist.ltacvars, TacMatch (intern_tactic ist c,intern_match_rule ist lmr)
   | TacId -> ist.ltacvars, TacId
   | TacFail _ as x -> ist.ltacvars, x
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
@@ -1230,7 +1227,6 @@ and eval_tactic ist = function
   | TacFun (it,body) -> assert false
   | TacLetRecIn (lrc,u) -> assert false
   | TacLetIn (l,u) -> assert false
-  | TacLetCut l -> letcut_interp ist l
   | TacMatchContext _ -> assert false
   | TacMatch (c,lmr) -> assert false
   | TacId -> tclIDTAC
@@ -1347,15 +1343,16 @@ and interp_letin ist gl = function
       check_is_value v;
       (id,v):: (interp_letin ist gl tl)
   | ((loc,id),Some com,tce)::tl ->
-    let typ = interp_may_eval pf_interp_constr ist gl com
+    let env = pf_env gl in
+    let typ = constr_of_value env (val_interp ist gl com)
     and v = interp_tacarg ist gl tce in
     let csr = 
       try
-	constr_of_value (pf_env gl) v
+	constr_of_value env v
       with Not_found ->
       try
 	let t = tactic_of_value v in
-	let ndc = Environ.named_context (pf_env gl) in
+	let ndc = Environ.named_context env in
 	start_proof id IsLocal ndc typ (fun _ _ -> ());
 	by t;
 	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
@@ -1367,32 +1364,6 @@ and interp_letin ist gl = function
           (str "Term or fully applied tactic expected in Let")
     in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl)
 
-(* Interprets the clauses of a LetCut *)
-and letcut_interp ist = function 
-  | [] -> tclIDTAC
-  | (id,c,tce)::tl -> fun gl ->
-    let typ = interp_constr_may_eval ist gl c
-    and v = interp_tacarg ist gl tce in
-    let csr = 
-      try
-	constr_of_value (pf_env gl) v
-      with Not_found ->
-      try
-	let t = tactic_of_value v in
-	start_proof id IsLocal (pf_hyps gl) typ (fun _ _ -> ());
-	by t;
-	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
-	delete_proof (dummy_loc,id);
-        pft
-      with | NotTactic ->
-	delete_proof (dummy_loc,id);
-	errorlabstrm "Tacinterp.interp_letin"
-          (str "Term or fully applied tactic expected in Let")
-    in
-    let cutt = h_cut typ
-    and exat = h_exact csr in
-    tclTHENSV cutt [|tclTHEN (introduction id) (letcut_interp ist tl);exat|] gl
-
 (* Interprets the Match Context expressions *)
 and match_context_interp ist g lr lmr =
   let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
@@ -1561,8 +1532,8 @@ and match_interp ist g constr lmr =
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for Match") in
-  let csr = interp_constr_may_eval ist g constr in
   let env = pf_env g in
+  let csr = constr_of_value env (val_interp ist g constr) in
   let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in
   apply_match ist csr ilr
 
@@ -1927,15 +1898,12 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
       TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
   | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,option_app (subst_raw_may_eval subst) c,subst_tacarg subst b)) l in
+      let l = List.map (fun (n,c,b) -> (n,option_app (subst_tactic subst) c,subst_tacarg subst b)) l in
       TacLetIn (l,subst_tactic subst u)
-  | TacLetCut l ->
-      let f (n,c,t) = (n,subst_raw_may_eval subst c,subst_tacarg subst t) in
-      TacLetCut (List.map f l)
   | TacMatchContext (lr,lmr) ->
       TacMatchContext(lr, subst_match_rule subst lmr)
   | TacMatch (c,lmr) ->
-      TacMatch (subst_raw_may_eval subst c,subst_match_rule subst lmr)
+      TacMatch (subst_tactic subst c,subst_match_rule subst lmr)
   | TacId | TacFail _ as x -> x
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ec05d2b40..c9a5c2cc0 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -55,13 +55,13 @@ let is_disj ist =
 let not_dep_intros ist =
   <:tactic<
   repeat match context with
-  | [|- (?X1 -> ?X2) ] => intro
-  | [|- (Coq.Init.Logic.iff _ _)] => unfold Coq.Init.Logic.iff
-  | [|- (Coq.Init.Logic.not _)]   => unfold Coq.Init.Logic.not
-  | [ H:(Coq.Init.Logic.iff _ _)|- _] => unfold Coq.Init.Logic.iff in H
-  | [ H:(Coq.Init.Logic.not _)|-_]    => unfold Coq.Init.Logic.not in H
-  | [ H:(Coq.Init.Logic.iff _ _)->_|- _] => unfold Coq.Init.Logic.iff in H
-  | [ H:(Coq.Init.Logic.not _)->_|-_]    => unfold Coq.Init.Logic.not in H
+  | |- (?X1 -> ?X2) => intro
+  | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff
+  | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not
+  | H:(Coq.Init.Logic.iff _ _)|- _ => unfold Coq.Init.Logic.iff in H
+  | H:(Coq.Init.Logic.not _)|-_    => unfold Coq.Init.Logic.not in H
+  | H:(Coq.Init.Logic.iff _ _)->_|- _ => unfold Coq.Init.Logic.iff in H
+  | H:(Coq.Init.Logic.not _)->_|-_    => unfold Coq.Init.Logic.not in H
   end >>
 				      
 let axioms ist =
@@ -69,9 +69,9 @@ let axioms ist =
   and t_is_empty = tacticIn is_empty in
     <:tactic<
     match reverse context with
-      |[|- ?X1] => $t_is_unit; constructor 1
-      |[_:?X1 |- _] => $t_is_empty; elimtype X1; assumption
-      |[_:?X1 |- ?X1] => assumption
+      | |- ?X1 => $t_is_unit; constructor 1
+      | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
+      | _:?X1 |- ?X1 => assumption
     end >>
 
 
@@ -84,27 +84,27 @@ let simplif ist =
     $t_not_dep_intros;
     repeat
        (match reverse context with
-        | [id: (?X1 _ _) |- _] =>
+        | id: (?X1 _ _) |- _ =>
             $t_is_conj; elim id; do 2 intro; clear id
-        | [id: (?X1 _ _) |- _] => $t_is_disj; elim id; intro; clear id
-        | [id0: ?X1-> ?X2, id1: ?X1|- _] =>
+        | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id
+        | id0: ?X1-> ?X2, id1: ?X1|- _ =>
 	    (* generalize (id0 id1); intro; clear id0 does not work
 	       (see Marco Maggiesi's bug PR#301)
 	    so we instead use Assert and exact. *)
 	    assert X2; [exact (id0 id1) | clear id0]
-        | [id: ?X1 -> ?X2|- _] =>
+        | id: ?X1 -> ?X2|- _ =>
           $t_is_unit; cut X2;
 	    [ intro; clear id
 	    | (* id : ?X1 -> ?X2 |- ?X2 *)
 	      cut X1; [exact id| constructor 1; fail]
 	    ]
-        | [id: (?X1 ?X2 ?X3) -> ?X4|- _] =>
+        | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
           $t_is_conj; cut (X2-> X3-> X4);
 	    [ intro; clear id
 	    | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X3 -> ?X4 *)
 	      intro; intro; cut (X1 X2 X3); [exact id| split; assumption]
 	    ]
-        | [id: (?X1 ?X2 ?X3) -> ?X4|- _] =>
+        | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
           $t_is_disj;
 	    cut (X3-> X4);
 	      [cut (X2-> X4);
@@ -115,7 +115,7 @@ let simplif ist =
 	      | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X3 -> ?X4 *)
 		intro; cut (X1 X2 X3); [exact id| right; assumption]
 	      ]
-        | [|- (?X1 _ _)] => $t_is_conj; split
+        | |- (?X1 _ _) => $t_is_conj; split
         end;
         $t_not_dep_intros) >>
 
@@ -128,20 +128,20 @@ let rec tauto_intuit t_reduce solver ist =
   <:tactic<
    ($t_simplif;$t_axioms
    || match reverse context with
-      | [id:(?X1-> ?X2)-> ?X3|- _] =>
+      | id:(?X1-> ?X2)-> ?X3|- _ =>
 	  cut X3;
 	    [ intro; clear id; $t_tauto_intuit 
 	    | cut (X1 -> X2);
 		[ exact id
 		| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
 		  solve [ $t_tauto_intuit ]]]
-      | [|- (?X1 _ _)] =>
+      | |- (?X1 _ _) =>
           $t_is_disj; solve [left;$t_tauto_intuit | right;$t_tauto_intuit]
       end
     ||
     (* NB: [|- _ -> _] matches any product *)
-    match context with |[ |- _ -> _ ] => intro; $t_tauto_intuit
-    |[ |- _ ] => $t_reduce;$t_solver
+    match context with | |- _ -> _ => intro; $t_tauto_intuit
+    |  |- _  => $t_reduce;$t_solver
     end
     ||
     $t_solver
@@ -150,8 +150,8 @@ let rec tauto_intuit t_reduce solver ist =
 let reduction_not_iff=interp
  <:tactic<repeat 
   match context with 
-  | [ |- _ ] => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff 
-  | [ H:_ |- _ ] => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
+  | |- _     => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff 
+  | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
   end >>
 
 
@@ -174,7 +174,7 @@ let default_intuition_tac = interp <:tactic< auto with * >>
 let q_elim tac=
   <:tactic<
   match context with 
-  [ x : ?X1, H : ?X1 -> _ |- _ ] => generalize (H x); clear H; $tac
+    x : ?X1, H : ?X1 -> _ |- _ => generalize (H x); clear H; $tac
   end >>
 
 let rec lfo n gl=
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 0b7b630e4..8a107f5c0 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -85,7 +85,7 @@ Uninterpreted Notation "B + { x : A & P & Q }"
 (* At level 1 to factor with {x:A|P} etc *)
 
 Uninterpreted Notation "{ A }  + { B }" (at level 1)
-  V8only (at level 10, A at level 80).
+  V8only (at level 0, A at level 80).
 
 Uninterpreted Notation "A + { B }" (at level 4, left associativity)
   V8only (at level 40, B at level 80, left associativity).
@@ -93,13 +93,13 @@ Uninterpreted Notation "A + { B }" (at level 4, left associativity)
 (** Notations for sigma-types or subsets *)
 
 Uninterpreted Notation "{ x : A  |  P }" (at level 1)
-  V8only (at level 10, x at level 80).
+  V8only (at level 0, x at level 80).
 Uninterpreted Notation "{ x : A  |  P  &  Q }" (at level 1)
-  V8only (at level 10, x at level 80).
+  V8only (at level 0, x at level 80).
 
 Uninterpreted Notation "{ x : A  &  P }" (at level 1)
-  V8only (at level 10, x at level 80).
+  V8only (at level 0, x at level 80).
 Uninterpreted Notation "{ x : A  &  P  &  Q }" (at level 1)
-  V8only (at level 10, x at level 80).
+  V8only (at level 0, x at level 80).
 
 Delimits Scope type_scope with T.
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index cf8c57ae9..3e50cdb09 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -238,40 +238,41 @@ let pr_induction_kind = function
 
 let pr_match_pattern pr_pat = function
   | Term a -> pr_pat a
-  | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
-  | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+  | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]"
+  | Subterm (Some id,a) ->
+      str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
 let pr_match_hyps pr_pat = function
   | Hyp (nal,mp) -> pr_located pr_name nal ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
-      str "[" ++ pr_match_pattern pr_pat mp ++ str "]"
-      ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
+      pr_match_pattern pr_pat mp ++
+      spc () ++ str "=>" ++ brk (1,4) ++ pr t
   | Pat (rl,mp,t) ->
-      str "[" ++ prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
+      prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
       spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
-      str "] =>" ++ brk (1,4) ++ pr t
+      str "=>" ++ brk (1,4) ++ pr t
   | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
 let pr_funvar = function
   | None -> spc () ++ str "()"
   | Some id -> spc () ++ pr_id id
 
-let pr_let_clause k pr prc pr_cst = function
+let pr_let_clause k pr = function
   | (id,None,t) ->
       hov 0 (str k ++ pr_located pr_id id ++ str " :=" ++ brk (1,1) ++
              pr (TacArg t))
   | (id,Some c,t) ->
       hv 0 (str k ++ pr_located pr_id id ++ str" :" ++ brk(1,2) ++
-      pr_may_eval prc prc pr_cst c ++
+      pr c ++
       str " :=" ++ brk (1,1) ++ pr (TacArg t))
 
-let pr_let_clauses pr prc pr_cst = function
+let pr_let_clauses pr = function
   | hd::tl ->
       hv 0
-        (pr_let_clause "let " pr prc pr_cst hd ++
-         prlist (fun t -> spc () ++ pr_let_clause "with " pr prc pr_cst t) tl)
+        (pr_let_clause "let " pr hd ++
+         prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
   | [] -> anomaly "LetIn must declare at least one binding"
 
 let pr_rec_clause pr (id,(l,t)) =
@@ -604,15 +605,12 @@ let rec pr_tac env inherited tac =
       llet
   | TacLetIn (llc,u) ->
       v 0
-       (hv 0 (pr_let_clauses (pr_tac env ltop) (pr_constr env) (pr_cst env) llc
+       (hv 0 (pr_let_clauses (pr_tac env ltop) llc
        ++ str " in") ++
        fnl () ++ pr_tac env (llet,E) u),
       llet
-  | TacLetCut llc -> assert false
   | TacMatch (t,lrul) ->
-      hov 0 (str "match " ++
-             pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) t
-        ++ str " with"
+      hov 0 (str "match " ++ pr_tac env ltop t ++ str " with"
         ++ prlist
 	  (fun r -> fnl () ++ str "| " ++
             pr_match_rule true (pr_tac env ltop) pr_pat r)