Bugs, nettoyage, et améliorations diverses

- vérification de la cohérence des ident pour éviter une option -R
  avec des noms non parsables (la vérification est faite dans
  id_of_string ce qui est très exigeant; faudrait-il une solution plus
  souple ?)
- correction message d'erreur inapproprié dans le apply qui descend dans les 
  conjonctions
- nettoyage autour de l'échec en présence de métas dans le prim_refiner
- nouveau message d'erreur quand des variables ne peuvent être instanciées
- quelques simplifications et davantage de robustesse dans inversion
- factorisation du code de constructor and co avec celui de econstructor and co

Documentation des tactiques
- edestruct/einduction/ecase/eelim et nouveautés apply
- nouvelle sémantique des intropatterns disjonctifs et documentation des
  pattern -> et <-
- relecture de certaines parties du chapitre tactique


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

51 files changed, 807 insertions, 637 deletions

diff --git a/CHANGES b/CHANGES
index fb0250c58..3f8742618 100644
--- a/CHANGES
+++ b/CHANGES
@@ -109,9 +109,12 @@ Tactic Language
   generated by expr_0. In this case, the value of expr (or idtac in
   case of just "..") is applied to the intermediate subgoals to make
   the number of tactics equal to the number of subgoals.
-- Names to be used as actual identifiers (like f in "apply f_equal f:=t")
-  must not be used elsewhere as variables in the same ltac expression
-  (possible source of incompatibility).
+- A name used as the name of the parameter of a lemma (like f in
+  "apply f_equal with (f:=t)") is now interpreted as a ltac variable
+  if such a variable exists (this is a possible source of
+  incompatibility and it can be fixed by renaming the variables of a
+  ltac function into names that do not clash with the lemmas
+  parameter names used in the tactic).
 - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
 - "let rec ... in ... " now supports for expressions without explicit
   parameters; interpretation is lazy to the contrary of "let ... in ...";
@@ -169,7 +172,8 @@ Type Classes
   Relation_Definitions.
 - New experimental "setoid" rewriting tactic based on typeclasses.
   Classes.Morphisms declares standard morphisms, Classes.Equivalence declares 
-  the new Setoid typeclass and some derived tactics.
+  the new Setoid typeclass and some derived tactics (source of
+  incompatibilities: 1- Setoid has to be required first 2- ...)
   
 Program
 
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index fe41b96cb..ac32f6abe 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -120,7 +120,7 @@ type side = Hyp | Concl | Hint
 
 let no_atoms = (false,{positive=[];negative=[]})
 
-let dummy_id=VarRef (id_of_string "")
+let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *)
 
 let build_atoms gl metagen side cciterm =
   let trivial =ref false
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index a18185168..b6112e653 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -78,7 +78,7 @@ let and_tac backtrack continue seq=
 
 let or_tac backtrack continue seq=
   tclORELSE 
-    (any_constructor (Some (tclCOMPLETE (wrap 0 true continue seq))))
+    (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
     backtrack
 
 let arrow_tac backtrack continue seq=
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index c5f850975..d1527c58a 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -337,11 +337,11 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacRevert    _ -> acc
 
     (* Constructors *)
-    | TacLeft        cb
-    | TacRight       cb
-    | TacSplit       (_, cb)
-    | TacConstructor (_, cb) -> depends_of_'a_bindings depends_of_'constr cb acc
-    | TacAnyConstructor taco -> Option.fold_right depends_of_'tac taco acc
+    | TacLeft        (_,cb)
+    | TacRight       (_,cb)
+    | TacSplit       (_, _, cb)
+    | TacConstructor (_, _, cb) -> depends_of_'a_bindings depends_of_'constr cb acc
+    | TacAnyConstructor (_,taco) -> Option.fold_right depends_of_'tac taco acc
 
     (* Conversion *)
     | TacReduce  (reg,_) ->
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 0680cc23e..c16cde7d7 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -163,12 +163,12 @@ let make_pbp_atomic_tactic = function
   | PbpTryAssumption (Some a) ->
       TacTry (TacAtom (zz, TacExact (make_var a)))
   | PbpExists x -> 
-      TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x]))
+      TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x]))
   | PbpGeneralize (h,args) ->
       let l = List.map make_pbp_pattern args in
       TacAtom (zz, TacGeneralize [make_app (make_var h) l])
-  | PbpLeft -> TacAtom (zz, TacLeft NoBindings)
-  | PbpRight -> TacAtom (zz, TacRight NoBindings)
+  | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings))
+  | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
   | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
@@ -178,7 +178,7 @@ let make_pbp_atomic_tactic = function
 	(zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
       TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
-  | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
+  | PbpSplit -> TacAtom (zz, TacSplit (false,false,NoBindings));;
 
 let rec make_pbp_tactic = function
   | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 20c1cc04f..7f2019681 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1183,8 +1183,8 @@ let rec natural_ntree ig ntree =
 	    TacIntroPattern _ -> natural_intros ig lh g gs ltree
 	  | TacIntroMove _ -> natural_intros ig lh g gs ltree
 	  | TacFix (_,n) -> natural_fix ig lh g gs n ltree
-	  | TacSplit (_,NoBindings) -> natural_split ig lh g gs ge [] ltree
-	  | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree
+	  | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree
+	  | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree
 	  | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd l) ltree
 	  | TacRight _ -> natural_right ig lh g gs ltree
 	  | TacLeft _ -> natural_left ig lh g gs ltree
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 63efd543a..16a95d065 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -976,10 +976,12 @@ and xlate_tac =
     | TacIntroMove (Some id, None) ->
      CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
     | TacIntroMove (None, None) ->  CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
-    | TacLeft bindl -> CT_left (xlate_bindings bindl)
-    | TacRight bindl -> CT_right (xlate_bindings bindl)
-    | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
-    | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
+    | TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
+    | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
+    | TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacSplit _ | TacRight _ | TacLeft _ -> 
+	xlate_error "TODO: esplit, eright, etc"
     | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
 	let c1 = xlate_formula (out_gen rawwit_constr c1) in
 	let c2 = xlate_formula (out_gen rawwit_constr c2) in
@@ -1149,9 +1151,10 @@ and xlate_tac =
     | TacApply (true,true,(c,bindl)) ->
      CT_eapply (xlate_formula c, xlate_bindings bindl)
     | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
-    | TacConstructor (n_or_meta, bindl) ->
+    | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
+    | TacConstructor _ -> xlate_error "TODO: econstructor"
     | TacSpecialize (nopt, (c,sl)) ->
      CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
     | TacGeneralize [] -> xlate_error ""
@@ -1239,11 +1242,12 @@ and xlate_tac =
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
-    | TacAnyConstructor(Some tac) -> 
+    | TacAnyConstructor(false,Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
-    | TacAnyConstructor(None) -> 
+    | TacAnyConstructor(false,None) -> 
 	CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none)
+    | TacAnyConstructor _ -> xlate_error "TODO: econstructor"
     | TacExtend(_, "ring", [args]) -> 
 	CT_ring
 	  (CT_formula_list
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index aa59daf5f..b96b57d5b 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -128,7 +128,7 @@ let intern_id,unintern_id =
     
 let mk_then = tclTHENLIST
 
-let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c])
+let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c])
 
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 1bc5897c4..6863a1885 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1705,7 +1705,7 @@ let vars_of_ctx ctx =
 	    match na with
 		Anonymous -> raise (Invalid_argument "vars_of_ctx")
 	      | Name n -> n, RVar (dummy_loc, n) :: vars)
-      ctx (id_of_string "vars_of_ctx: error", [])
+      ctx (id_of_string "vars_of_ctx_error", [])
   in List.rev y
 
 let rec is_included x y = 
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index cb3873bdf..2a8e2e5d9 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -79,7 +79,7 @@ let type_ctx_instance isevars env ctx inst subst =
 	(na, c) :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
-let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))
+(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*)
 
 let type_class_instance_params isevars env id n ctx inst subst =
   List.fold_left2
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index dc79597dd..91bf626b1 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -238,7 +238,7 @@ let build_dependent_sum l =
 	     (tclTHENS tac
 		([intros;
 		  (tclTHENSEQ 
-		     [constructor_tac (Some 1) 1 
+		     [constructor_tac false (Some 1) 1 
 			(Rawterm.ImplicitBindings [inj_open (mkVar n)]);
 		      cont]);
 		 ])))
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 75e428e14..5515320f0 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -57,16 +57,6 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
 let get_uri_of_var v pvars =
  let module D = Declare in
  let module N = Names in
-  let rec search_in_pvars names =
-   function
-      [] -> None
-    | ((name,l)::tl) ->
-       let names' = name::names in
-        if List.mem v l then
-         Some names'
-        else
-         search_in_pvars names' tl
-  in
   let rec search_in_open_sections =
    function
       [] -> Util.error ("Variable "^v^" not found")
@@ -78,9 +68,10 @@ let get_uri_of_var v pvars =
          search_in_open_sections tl
   in
    let path =
-    match search_in_pvars [] pvars with
-       None -> search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
-     | Some path -> path
+    if List.mem v pvars then
+      []
+    else
+      search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3a0fdfb9b..649139f35 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -89,8 +89,7 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 (* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT   *)
 (* SECTION, WHOSE PATH IS namei                                     *)
 
-let pvars =
- ref ([Names.id_of_string "",[]] : (Names.identifier * string list) list);;
+let pvars = ref ([] : string list);;
 let cumenv = ref Environ.empty_env;;
 
 (* filter_params pvars hyps *)
@@ -138,9 +137,7 @@ let add_to_pvars x =
          E.push_named (Names.id_of_string v, None, typ) !cumenv ;
        v
   in
-   match !pvars with
-      []       -> assert false
-    | ((name,l)::tl) -> pvars := (name,v::l)::tl
+  pvars := v::!pvars
 ;;
 
 (* The computation is very inefficient, but we can't do anything *)
diff --git a/dev/base_include b/dev/base_include
index 792330726..83e23d29f 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -19,6 +19,7 @@
 
 #install_printer  (* identifier *) ppid;;
 #install_printer  (* identifier *) ppidset;;
+#install_printer  (* Intset.t *) ppintset;;
 #install_printer  (* label *) pplab;;
 #install_printer  (* mod_self_id *) ppmsid;;
 #install_printer  (* mod_bound_id *) ppmbid;;
diff --git a/dev/db b/dev/db
index dc323ec47..e668f1e86 100644
--- a/dev/db
+++ b/dev/db
@@ -3,6 +3,7 @@ load_printer "printers.cma"
 
 install_printer Top_printers.ppid
 install_printer Top_printers.ppidset
+install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
 install_printer Top_printers.ppmsid
 install_printer Top_printers.ppmbid
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 07dda42b8..c06738226 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -62,7 +62,9 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let ppbigint n = pp (Bigint.pr_bigint n);;
 
-let ppidset l = pp (prlist_with_sep spc pr_id (Idset.elements l))
+let prset pr l = str "[" ++ prlist_with_sep spc pr l ++ str "]"
+let ppintset l = pp (prset int (Intset.elements l))
+let ppidset l = pp (prset pr_id (Idset.elements l))
 
 let pP s = pp (hov 0 s)
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index d5935ed34..59217b352 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -83,7 +83,7 @@ displayed as in \Coq\ terms.
 
 \SeeAlso Chapter~\ref{Extraction}.
 
-\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold the
+\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold
 the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
 $\delta$-conversion. Unfolding a constant is replacing it by its
 definition. {\tt Opaque} can only apply on constants originally
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index bac155bb5..c80532d23 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1,3 +1,5 @@
+% TODO: unify the use of \form and \type to mean a type
+% or use \form specifically for a type of type Prop
 \chapter{Tactics
 \index{Tactics}
 \label{Tactics}}
@@ -104,7 +106,7 @@ An example of use is given in Section~\ref{refine-example}.
 \index{Typing rules}}
 
 Tactics presented in this section implement the basic typing rules of
-{\sc Cic} given in Chapter~\ref{Cic}.
+{\CIC} given in Chapter~\ref{Cic}.
 
 \subsection{{\tt assumption}
 \tacindex{assumption}}
@@ -346,10 +348,22 @@ This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context.  The tactic {\tt apply} tries to
 match the current goal against the conclusion of the type of {\term}.
 If it succeeds, then the tactic returns as many subgoals as the number
-of non dependent premises of the type of {\term}.  The tactic {\tt
-apply} relies on first-order pattern-matching with dependent
-types. See {\tt pattern} in Section~\ref{pattern} to transform a
-second-order pattern-matching problem into a first-order one.
+of non dependent premises of the type of {\term}. If the conclusion of
+the type of {\term} does not match the goal {\tt and} the conclusion
+is an inductive type isomorphic to a tuple type, then each component
+of the tuple is recursively matched to the goal in the left-to-right
+order.
+
+The tactic {\tt apply} relies on first-order unification with
+dependent types unless the conclusion of the type of {\term} is of the
+form {\tt ($P$~ $t_1$~\ldots ~$t_n$)} with $P$ to be instantiated.  In
+the latter case, the behavior depends on the form of the goal. If the
+goal is of the form {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$} and the
+$t_i$ and $u_i$ unifies, then $P$ is taken to be (fun $x$ => $Q$).
+Otherwise, {\tt apply} tries to define $P$ by abstracting over
+$t_1$~\ldots ~$t_n$ in the goal. See {\tt pattern} in
+Section~\ref{pattern} to transform the goal so that it gets the form
+{\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}.
 
 \begin{ErrMsgs}
 \item \errindex{Impossible to unify \dots\ with \dots} 
@@ -360,9 +374,10 @@ second-order pattern-matching problem into a first-order one.
   goal with the {\tt change} or {\tt pattern} tactics (see 
   sections~\ref{pattern},~\ref{change}).
 
-\item \errindex{generated subgoal {\term'} has metavariables in it}
+\item \errindex{Unable to find an instance for the variables
+{\ident} \ldots {\ident}}
 
-  This occurs when some instantiations of premises of {\term} are not
+  This occurs when some instantiations of the premises of {\term} are not
   deducible from the unification. This is the case, for instance, when
   you want to apply a transitivity property. In this case, you have to
   use one of the variants below:
@@ -597,7 +612,7 @@ This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context and the argument {\ident} is an
 hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
 tries to match the conclusion of the type of {\ident} against a non
-dependent premisses of the type of {\term}, trying them from right to
+dependent premises of the type of {\term}, trying them from right to
 left.  If it succeeds, the statement of hypothesis {\ident} is
 replaced by the conclusion of the type of {\ident}. The tactic also
 returns as many subgoals as the number of other non dependent premises
@@ -624,7 +639,7 @@ This applies each of {\term} in sequence in {\ident}.
 \item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
 
 This does the same but uses the bindings in each {\bindinglist} to 
-instanciate the parameters of the corresponding type of {\term}
+instantiate the parameters of the corresponding type of {\term}
 (see syntax of bindings in Section~\ref{Binding-list}).
 
 \end{Variants}
@@ -721,23 +736,39 @@ This tactic applies to any goal. It implements the rule
 \index{Binding list}
 \label{Binding-list}}
 
-A bindings list is generally used after the keyword {\tt with} in
-tactics.  The general shape of a bindings list is {\tt (\vref$_1$ :=
-  \term$_1$) \dots\ (\vref$_n$ := \term$_n$)} where {\vref} is either an
-{\ident} or a {\num}. It is used to provide a tactic with a list of
-values (\term$_1$, \dots, \term$_n$) that have to be substituted
-respectively to \vref$_1$, \dots, \vref$_n$. For all $i \in [1\dots\ 
-n]$, if \vref$_i$ is \ident$_i$ then it references the dependent
-product {\tt \ident$_i$:T} (for some type \T); if \vref$_i$ is
-\num$_i$ then it references the \num$_i$-th non dependent premise.
-
-A bindings list can also be a simple list of terms {\tt \term$_1$
-  \term$_2$ \dots\term$_n$}. In that case the references to which
-these terms correspond are determined by the tactic. In case of {\tt
-  elim} (see Section~\ref{elim}) the terms should correspond to
-all the dependent products in the type of \term\ while in the case of
-{\tt apply} only the dependent products which are not bound in
-the conclusion of the type are given.
+Tactics that take a term as argument may also support bindings list so
+as to instantiate some parameters of the term by name or position.
+The general form of a term equipped with a bindings list is {\tt
+{\term} with {\bindinglist}} where {\bindinglist} may be of two
+different forms:
+
+\begin{itemize}
+\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$)
+  \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a
+  {\num}. The references are determined according to the type of
+  {\term}. If \vref$_i$ is an identifier, this identifier has to be
+  bound in the type of {\term} and the binding provides the tactic
+  with an instance for the parameter of this name.  If \vref$_i$ is
+  some number $n$, this number denotes the $n$-th non dependent
+  premise of the {\term}, as determined by the type of {\term}.
+
+  \ErrMsg \errindex{No such binder}
+
+\item A bindings list can also be a simple list of terms {\tt
+  \term$_1$ \term$_2$ \dots\term$_n$}. In that case the references to
+  which these terms correspond are determined by the tactic. In case
+  of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see
+  Section~\ref{elim}) the terms have to provide instances for all the
+  dependent products in the type of \term\ while in the case of {\tt
+  apply}, or of {\tt constructor} and its variants, only instances for
+  the dependent products which are not bound in the conclusion of the
+  type are required.
+
+  \ErrMsg \errindex{Not the right number of missing arguments}
+
+\end{itemize}
+
+
 
 \subsection{\tt evar (\ident:\term)
 \tacindex{evar}
@@ -869,22 +900,22 @@ performs the conversion in hypotheses $H_1\ldots H_n$.
 \tacindex{vm\_compute}\label{vmcompute}}
 
 These parameterized reduction tactics apply to any goal and perform
-the normalization of the goal according to the specified flags. Since
-the reduction considered in \Coq\ include $\beta$ (reduction of
-functional application), $\delta$ (unfolding of transparent constants,
-see \ref{Transparent}), $\iota$ (reduction of {\tt Cases}, {\tt Fix}
-and {\tt CoFix} expressions) and $\zeta$ (removal of local
-definitions), every flag is one of {\tt beta}, {\tt delta}, {\tt
-  iota}, {\tt zeta}, {\tt [\qualid$_1$\ldots\qualid$_k$]} and {\tt
-  -[\qualid$_1$\ldots\qualid$_k$]}.  The last two flags give the list
-of constants to unfold, or the list of constants not to unfold. These
-two flags can occur only after the {\tt delta} flag. 
-If alone (i.e. not
-followed by {\tt [\qualid$_1$\ldots\qualid$_k$]} or {\tt
-  -[\qualid$_1$\ldots\qualid$_k$]}), the {\tt delta} flag means that all constants must be unfolded.
-However, the {\tt delta} flag does not apply to variables bound by a
-let-in construction whose unfolding is controlled by the {\tt
-  zeta} flag only.
+the normalization of the goal according to the specified flags. In
+correspondence with the kinds of reduction considered in \Coq\, namely
+$\beta$ (reduction of functional application), $\delta$ (unfolding of
+transparent constants, see \ref{Transparent}), $\iota$ (reduction of
+pattern-matching over a constructed term, and unfolding of {\tt fix}
+and {\tt cofix} expressions) and $\zeta$ (contraction of local
+definitions), the flag are either {\tt beta}, {\tt delta}, {\tt iota}
+or {\tt zeta}. The {\tt delta} flag itself can be refined into {\tt
+delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta
+-[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the
+constants to unfold to the constants listed, and restricting in the
+second case the constant to unfold to all but the ones explicitly
+mentioned. Notice that the {\tt delta} flag does not apply to
+variables bound by a let-in construction inside the term itself (use
+here the {\tt zeta} flag). In any cases, opaque constants are not
+unfolded (see Section~\ref{Opaque}).
 
 The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
 tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
@@ -892,8 +923,8 @@ is a call-by-need strategy, with sharing of reductions: the arguments of a
 function call are partially evaluated only when necessary, but if an
 argument is used several times, it is computed only once. This
 reduction is efficient for reducing expressions with dead code. For
-instance, the proofs of a proposition $\exists_T ~x. P(x)$ reduce to a
-pair of a witness $t$, and a proof that $t$ verifies the predicate
+instance, the proofs of a proposition {\tt exists~$x$. $P(x)$} reduce to a
+pair of a witness $t$, and a proof that $t$ satisfies the predicate
 $P$. Most of the time, $t$ may be computed without computing the proof
 of $P(t)$, thanks to the lazy strategy.
 
@@ -901,19 +932,37 @@ The call-by-value strategy is the one used in ML languages: the
 arguments of a function call are evaluated first, using a weak
 reduction (no reduction under the $\lambda$-abstractions). Despite the
 lazy strategy always performs fewer reductions than the call-by-value
-strategy, the latter should be preferred for evaluating purely
+strategy, the latter is generally more efficient for evaluating purely
 computational expressions (i.e. with few dead code).
 
 \begin{Variants}
-\item {\tt compute} \tacindex{compute} 
+\item {\tt compute} \tacindex{compute}\\
+      {\tt cbv}
   
-  This tactic is an alias for {\tt cbv beta delta iota zeta}.
+  These are synonyms for {\tt cbv beta delta iota zeta}.
 
-\item {\tt compute delta [\qualid$_1$\ldots\qualid$_k$]} (resp. {\tt compute delta  -[\qualid$_1$\ldots\qualid$_k$]})  \tacindex{compute} 
+\item {\tt lazy}
+  
+  This is a synonym for {\tt lazy beta delta iota zeta}.
 
-      This tactic is an alias for {\tt cbv beta delta iota zeta [\qualid$_1$\ldots\qualid$_k$]} (resp. {\tt cbv beta delta iota zeta -[\qualid$_1$\ldots\qualid$_k$]}) .
+\item {\tt compute [\qualid$_1$\ldots\qualid$_k$]}\\
+      {\tt cbv [\qualid$_1$\ldots\qualid$_k$]}
+
+  These are synonyms of {\tt cbv beta delta
+  [\qualid$_1$\ldots\qualid$_k$] iota zeta}.
   
-  This tactic is an alias for {\tt cbv beta delta iota zeta}.
+\item {\tt compute -[\qualid$_1$\ldots\qualid$_k$]}\\
+      {\tt cbv -[\qualid$_1$\ldots\qualid$_k$]}
+
+  These are synonyms of {\tt cbv beta delta
+  -[\qualid$_1$\ldots\qualid$_k$] iota zeta}.
+
+\item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\
+      {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]}
+
+  These are respectively synonyms of {\tt cbv beta delta
+  [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbv beta delta
+  -[\qualid$_1$\ldots\qualid$_k$] iota zeta}.
 
 \item {\tt vm\_compute} \tacindex{vm\_compute}
 
@@ -926,11 +975,12 @@ computational expressions (i.e. with few dead code).
 
 \end{Variants}
 
-\begin{ErrMsgs}
-\item \errindex{Delta must be specified before}
-  
-  A list of constants appeared before the {\tt delta} flag.
-\end{ErrMsgs}
+% Obsolete? Anyway not very important message
+%\begin{ErrMsgs}
+%\item \errindex{Delta must be specified before}
+%  
+%  A list of constants appeared before the {\tt delta} flag.
+%\end{ErrMsgs}
 
 
 \subsection{{\tt red}
@@ -1142,7 +1192,6 @@ equivalent to {\tt intros; apply ci}.
   the number of constructors of the head of the goal.
 
 \item {\tt constructor \num~with} {\bindinglist}
-  \tacindex{constructor \dots\  with}
   
   Let {\tt ci} be the {\tt i}-th constructor of {\tt I}, then {\tt
     constructor i with \bindinglist} is equivalent to {\tt intros;
@@ -1153,6 +1202,9 @@ equivalent to {\tt intros; apply ci}.
   context where {\tt apply} is executed (the introductions are not
   taken into account).
 
+% To document?
+% \item {\tt constructor {\tactic}}
+
 \item {\tt split}\tacindex{split}
 
   Applies if {\tt I} has only one constructor, typically in the case
@@ -1164,26 +1216,32 @@ equivalent to {\tt intros; apply ci}.
   case of existential quantification $\exists x\cdot P(x)$. 
   Then, it is equivalent to {\tt intros; constructor 1 with \bindinglist}.
 
-\item {\tt left}\tacindex{left},  {\tt right}\tacindex{right}
+\item {\tt left}\tacindex{left}\\
+      {\tt right}\tacindex{right}
 
   Apply if {\tt I} has two constructors, for instance in the case of
   disjunction $A\lor B$. Then, they are respectively equivalent to {\tt
     constructor 1} and {\tt constructor 2}.
   
-\item {\tt left \bindinglist}, {\tt right \bindinglist}, {\tt split
-    \bindinglist}
+\item {\tt left \bindinglist}\\
+      {\tt right \bindinglist}\\
+      {\tt split \bindinglist}
   
   As soon as the inductive type has the right number of constructors,
     these expressions are equivalent to the corresponding {\tt
     constructor $i$ with \bindinglist}.
 
-\item \texttt{econstructor}
+\item \texttt{econstructor}\tacindex{econstructor}\\
+      \texttt{eexists}\tacindex{eexists}\\
+      \texttt{esplit}\tacindex{esplit}\\
+      \texttt{eleft}\tacindex{eleft}\\
+      \texttt{eright}\tacindex{eright}\\
 
-  This tactic behaves like \texttt{constructor} but is able to
-  introduce existential variables if an instanciation for a variable
-  cannot be found (cf \texttt{eapply}). The tactics \texttt{eexists},
-  \texttt{esplit}, \texttt{eleft} and \texttt{eright} follows the same
-  behaviour.
+  These tactics and their variants behave like \texttt{constructor},
+  \texttt{exists}, \texttt{split}, \texttt{left}, \texttt{right} and
+  their variants but they introduce existential variables instead of
+  failing when the instantiation of a variable cannot be found (cf
+  \texttt{eapply} and Section~\ref{eapply-example}).
 
 \end{Variants}
 
@@ -1215,7 +1273,7 @@ There are particular cases:
 
 \item If {\term} is an identifier {\ident} denoting a quantified
 variable of the conclusion of the goal, then {\tt induction {\ident}}
-behaves as {\tt intros until {\ident}; induction {\ident}}
+behaves as {\tt intros until {\ident}; induction {\ident}}.
 
 \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt induction} applied to the
@@ -1236,9 +1294,10 @@ induction n.
 
 \begin{ErrMsgs}
 \item \errindex{Not an inductive product}
-\item \errindex{Cannot refine to conclusions with meta-variables}
+\item \errindex{Unable to find an instance for the variables
+{\ident} \ldots {\ident}}
   
-  As {\tt induction} uses {\tt apply}, see Section~\ref{apply} and
+  Use in this case 
   the variant {\tt elim \dots\ with \dots} below.
 \end{ErrMsgs}
 
@@ -1246,7 +1305,7 @@ induction n.
 \item{\tt induction {\term} as {\intropattern}}
   
   This behaves as {\tt induction {\term}} but uses the names in
-  {\intropattern} to names the variables introduced in the context.
+  {\intropattern} to name the variables introduced in the context.
   The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
   $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
     ]} with $m$ being the number of constructors of the type of
@@ -1254,7 +1313,7 @@ induction n.
   of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
   $p_{in_i}$ in order. If there are not enough names, {\tt induction}
   invents names for the remaining variables to introduce. More
-  generally, the $p$'s can be any introduction patterns (see
+  generally, the $p_{ij}$ can be any introduction patterns (see
   Section~\ref{intros-pattern}). This provides a concise notation for
   nested induction.
 
@@ -1262,68 +1321,89 @@ induction n.
 {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
 {\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
 
-\item {\tt induction {\term} using {\qualid}}
+\item{\tt induction {\term} with \bindinglist}
+
+  This behaves like \texttt{induction {\term}} providing explicit
+  instances for the premises of the type of {\term} (see the syntax of
+  bindings in Section~\ref{Binding-list}).
+
+\item{\tt einduction {\term}\tacindex{einduction}}
+
+  This tactic behaves like \texttt{induction {\term}} excepts that it
+  does not fail if some dependent premise of the type of {\term} is
+  not inferable. Instead, the unresolved premises are posed as
+  existential variables to be inferred later, in the same way as {\tt
+  eapply} does (see Section~\ref{eapply-example}).
+
+\item {\tt induction {\term$_1$} using {\term$_2$}}
 
-  This behaves as {\tt induction {\term}} but using the induction
-scheme of name {\qualid}. It does not expect that the type of
-{\term} is inductive.
+  This behaves as {\tt induction {\term$_1$}} but using {\term$_2$} as
+  induction scheme. It does not expect the conclusion of the type of
+  {\term} to be inductive.
+
+\item {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}
+
+  This behaves as {\tt induction {\term$_1$} using {\term$_2$}} but
+  also providing instances for the premises of the type of {\term$_2$}.
 
 \item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
 
-  where {\qualid} is an induction principle with complex predicates
-  (like the ones generated by function induction).
+  This syntax is used for the case {\qualid} denotes an induction principle
+  with complex predicates as the induction principles generated by
+  {\tt Function} or {\tt Functional Scheme} may be.
 
-\item {\tt induction {\term} as {\intropattern} using {\qualid}}
+\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\
+     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}
 
-  This combines {\tt induction {\term} using {\qualid}}
-and {\tt induction {\term} as {\intropattern}}.
+  This is the most general form of {\tt induction} and {\tt einduction}.
+  It combines the effects of the {\tt with}, {\tt as}, and {\tt
+  using} clauses.
 
 \item {\tt elim \term}\label{elim}
   
   This is a more basic induction tactic.  Again, the type of the
-  argument {\term} must be an inductive constant. Then according to
-  the type of the goal, the tactic {\tt elim} chooses the right
-  destructor and applies it (as in the case of the {\tt apply}
-  tactic). For instance, assume that our proof context contains {\tt
-    n:nat}, assume that our current goal is {\tt T} of type {\tt
-    Prop}, then {\tt elim n} is equivalent to {\tt apply nat\_ind with
-    (n:=n)}.  The tactic {\tt elim} does not affect the hypotheses of
+  argument {\term} must be an inductive type. Then, according to
+  the type of the goal, the tactic {\tt elim} chooses the appropriate
+  destructor and applies it as the tactic {\tt apply}
+  would do. For instance, if the proof context contains {\tt
+  n:nat} and the current goal is {\tt T} of type {\tt
+  Prop}, then {\tt elim n} is equivalent to {\tt apply nat\_ind with
+  (n:=n)}.  The tactic {\tt elim} does not modify the context of
   the goal, neither introduces the induction loading into the context
   of hypotheses.
 
-\item {\tt elim \term} 
-  
-  also works when the type of {\term} starts with products and the
-  head symbol is an inductive definition. In that case the tactic
-  tries both to find an object in the inductive definition and to use
-  this inductive definition for elimination.  In case of non-dependent
-  products in the type, subgoals are generated corresponding to the
-  hypotheses. In the case of dependent products, the tactic will try
-  to find an instance for which the elimination lemma applies.
+  More generally, {\tt elim \term} also works when the type of {\term}
+  is a statement with premises and whose conclusion is inductive.  In
+  that case the tactic performs induction on the conclusion of the
+  type of {\term} and leaves the non-dependent premises of the type as
+  subgoals.  In the case of dependent products, the tactic tries to
+  find an instance for which the elimination lemma applies and fails
+  otherwise.
 
-\item {\tt elim {\term} with \term$_1$ \dots\ \term$_n$}
-  \tacindex{elim \dots\ with} \
+\item {\tt elim {\term} with {\bindinglist}}
   
-  Allows the user to give explicitly the values for dependent
-  premises of the elimination schema. All arguments must be given.
+  Allows to give explicit instances to the premises of the type
+  of {\term} (see Section~\ref{Binding-list}).
 
-  \ErrMsg \errindex{Not the right number of dependent arguments}
+\item{\tt eelim {\term}\tacindex{eelim}}
 
-\item{\tt elim {\term} with ({\vref$_1$} := {\term$_1$}) \dots\ ({\vref$_n$}
-    := {\term$_n$}}) 
-  
-  Also provides {\tt elim} with values for instantiating premises by
-  associating explicitly variables (or non-dependent products) with
-  their intended instance (see \ref{Binding-list} for more details
-  about bindings list). 
+  In case the type of {\term} has dependent premises, this turns them into
+  existential variables to be resolved later on.
 
-\item{\tt elim {\term$_1$} using {\term$_2$}}
-\tacindex{elim \dots\ using} 
+\item{\tt elim {\term$_1$} using {\term$_2$}}\\
+     {\tt elim {\term$_1$} using {\term$_2$} with {\bindinglist}\tacindex{elim \dots\ using}}
 
 Allows the user to give explicitly an elimination predicate
 {\term$_2$} which is not the standard one for the underlying inductive
-type of {\term$_1$}. Each of the {\term$_1$} and {\term$_2$} is either
-a simple term or a term with a bindings list (see \ref{Binding-list}).
+type of {\term$_1$}. The {\bindinglist} clause allows to
+instantiate premises of the type of {\term$_2$}.
+
+\item{\tt elim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}\\
+     {\tt eelim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}
+
+  This is the most general form of {\tt elim} and {\tt eelim}.  It
+  combines the effects of the {\tt using} clause and of the two uses
+  of the {\tt with} clause.
 
 \item {\tt elimtype \form}\tacindex{elimtype}
   
@@ -1335,10 +1415,6 @@ a simple term or a term with a bindings list (see \ref{Binding-list}).
   in the goal then {\tt elim t} is equivalent to {\tt elimtype I; 2:
     exact t.}
 
-  \ErrMsg \errindex{Impossible to unify \dots\ with \dots} 
-  
-  Arises when {\form} needs to be applied to parameters.
-
 \item {\tt simple induction \ident}\tacindex{simple induction}
   
   This tactic behaves as {\tt intros until
@@ -1367,6 +1443,7 @@ a simple term or a term with a bindings list (see \ref{Binding-list}).
 
 \subsection{\tt destruct \term
 \tacindex{destruct}}
+\label{destruct}
 
 The tactic {\tt destruct} is used to perform case analysis without
 recursion. Its behavior is similar to {\tt induction} except
@@ -1377,7 +1454,7 @@ the type of {\term} must be inductively defined. There are particular cases:
 
 \item If {\term} is an identifier {\ident} denoting a quantified
 variable of the conclusion of the goal, then {\tt destruct {\ident}}
-behaves as {\tt intros until {\ident}; destruct {\ident}}
+behaves as {\tt intros until {\ident}; destruct {\ident}}.
 
 \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt destruct} applied to the
@@ -1392,7 +1469,7 @@ last introduced hypothesis.
 \item{\tt destruct {\term} as {\intropattern}}
   
   This behaves as {\tt destruct {\term}} but uses the names in
-  {\intropattern} to names the variables introduced in the context.
+  {\intropattern} to name the variables introduced in the context.
   The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
   $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
     ]} with $m$ being the number of constructors of the type of
@@ -1400,7 +1477,7 @@ last introduced hypothesis.
   of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
   $p_{in_i}$ in order. If there are not enough names, {\tt destruct}
   invents names for the remaining variables to introduce. More
-  generally, the $p$'s can be any introduction patterns (see
+  generally, the $p_{ij}$ can be any introduction patterns (see
   Section~\ref{intros-pattern}). This provides a concise notation for
   nested destruction.
 
@@ -1411,18 +1488,36 @@ last introduced hypothesis.
 {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
 {\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}.
 
-\item \texttt{pose proof {\term} as {\intropattern}}
+\item{\tt destruct {\term} with \bindinglist}
+
+  This behaves like \texttt{destruct {\term}} providing explicit
+  instances for the dependent premises of the type of {\term} (see
+  syntax of bindings in Section~\ref{Binding-list}).
+
+\item{\tt edestruct {\term}\tacindex{edestruct}}
+
+  This tactic behaves like \texttt{destruct {\term}} excepts that it
+  does not fail if the instance of a dependent premises of the type of
+  {\term} is not inferable. Instead, the unresolved instances are left
+  as existential variables to be inferred later, in the same way as
+  {\tt eapply} does (see Section~\ref{eapply-example}).
+
+\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
 
   This tactic behaves like \texttt{destruct {\term} as {\intropattern}}.
 
-\item{\tt destruct {\term} using {\qualid}}
+\item{\tt destruct {\term$_1$} using {\term$_2$}}\\
+     {\tt destruct {\term$_1$} using {\term$_2$} with {\bindinglist}}
 
-  This is a synonym of {\tt induction {\term} using {\qualid}}.
+  These are synonyms of {\tt induction {\term$_1$} using {\term$_2$}} and
+  {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}.
 
-\item{\tt destruct {\term} as {\intropattern} using {\qualid}}
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\
+     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\
 
-  This is a synonym of {\tt induction {\term} using {\qualid} as
-  {\intropattern}}.
+  This is the most general form of {\tt destruct} and {\tt edestruct}.
+  It combines the effects of the {\tt with}, {\tt as}, and {\tt
+  using} clauses.
 
 \item{\tt case \term}\label{case}\tacindex{case}
   
@@ -1438,11 +1533,17 @@ last introduced hypothesis.
  equalities between the original form of the term and the outcomes of 
  the case analysis. 
 
+\item {\tt case {\term} with {\bindinglist}}
 
-\item {\tt case {\term} with \term$_1$ \dots\ \term$_n$}
-  \tacindex{case \dots\ with}
+  Analogous to {\tt elim {\term} with {\bindinglist}} above.
 
-  Analogous to {\tt elim \dots\ with} above.
+\item{\tt ecase {\term}\tacindex{ecase}}\\
+  {\tt ecase {\term} with {\bindinglist}}
+  
+  In case the type of {\term} has dependent premises, or dependent
+  premises whose values are not inferable from the {\tt with
+  {\bindinglist}} clause, {\tt ecase} turns them into existential
+  variables to be resolved later on.
 
 \item {\tt simple destruct \ident}\tacindex{simple destruct}
   
@@ -1464,67 +1565,98 @@ last introduced hypothesis.
 \label{intros-pattern}
 \tacindex{intros \intropattern}}
 
-The tactic {\tt intros} applied to introduction patterns performs both
-introduction of variables and case analysis in order to give names to
-components of an hypothesis.
-
-An introduction pattern is either:
+This extension of the tactic {\tt intros} combines introduction of
+variables or hypotheses and case analysis. An introduction pattern is
+either:
 \begin{itemize}
 \item the wildcard: {\tt \_}
 \item the pattern \texttt{?}
 \item the pattern \texttt{?\ident}
-\item a variable
+\item an identifier
 \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
 \item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )}
+\item the rewriting orientations: {\tt ->} or {\tt <-}
 \end{itemize}
 
-The behavior of \texttt{intros} is defined inductively over the
-structure of the pattern given as argument:
+Assuming a goal of type {\tt $Q$ -> $P$} (non dependent product), or
+of type {\tt forall $x$:$T$, $P$} (dependent product), the behavior of
+{\tt intros $p$} is defined inductively over the structure of the
+introduction pattern $p$:
 \begin{itemize}
-\item introduction on the wildcard do the introduction and then
-  immediately clear (cf~\ref{clear}) the corresponding hypothesis;
-\item introduction on \texttt{?} do the introduction, and let Coq
+\item introduction on the wildcard depends on whether the product is
+  dependent or not: in the non dependent case, it erases the
+  corresponding hypothesis (i.e. it behaves as an {\tt intro} followed
+  by a {\tt clear}, cf Section~\ref{clear}) while in the dependent
+  case, it succeeds and erases the variable only if the wildcard is
+  part of a more complex list of introduction patterns that also
+  erases the hypotheses depending on this variable;
+\item introduction on \texttt{?} performs the introduction, and let {\Coq}
   choose a fresh name for the variable;
-\item introduction on \texttt{?\ident} do the introduction, and let Coq
-  choose a fresh name for the variable based on {\ident};
-\item introduction on a variable behaves like described in~\ref{intro}; 
-\item introduction over a
-list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of
-introductions over the patterns namely:
-\texttt{intros $p_1$;\ldots; intros $p_n$}, the goal should start with
-at least $n$ products;
-\item introduction over a
-disjunction of list of patterns
-{\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}. It introduces a new variable $X$, its type should be an inductive
-definition with $n$
-constructors, then it performs a case analysis over $X$ 
-(which generates $n$ subgoals), it 
-clears $X$ and performs on each generated subgoals the corresponding
-\texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$ tactic;
-\item introduction over a 
-conjunction  of patterns $(p_1,\ldots,p_n)$, it
-introduces a new variable $X$, its type should be an inductive 
-definition with $1$
-constructor with (at least) $n$ arguments, then it performs a case 
-analysis over $X$ 
-(which generates $1$ subgoal with at least $n$ products), it 
-clears $X$ and performs an introduction over the list of patterns $p_1~\ldots~p_n$.
+\item introduction on \texttt{?\ident} performs the introduction, and
+  let {\Coq} choose a fresh name for the variable based on {\ident};
+\item introduction on \texttt{\ident} behaves as described in
+  Section~\ref{intro};
+\item introduction over a disjunction of list of patterns {\tt
+  [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots}
+  $p_{nm_n}$]} expects the product to be over an inductive type whose
+  number of constructors is $n$ (or over a statement of conclusion a
+  similar inductive type ): it destructs the introduced hypothesis as
+  {\tt destruct} (see Section~\ref{destruct}) would and applies on
+  each generated subgoal the corresponding tactic
+  \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
+  pattern is part of a sequence of patterns and is not the last
+  pattern of the sequence, then {\Coq} completes the pattern so as all
+  the argument of the constructors of the inductive type are
+  introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H} applied
+  on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as the list
+  of patterns {\tt [$\,$|$\,$?$\,$] H});
+\item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
+  $p_n$)} expects the goal to be a product over an inductive type $I$ with a
+  single constructor that itself has at least $n$ arguments: it
+  performs a case analysis over the hypothesis, as {\tt destruct}
+  would, and applies the patterns $p_1$~\ldots~$p_n$ to the arguments
+  of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
+  $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
+  $p_n$]}).
+\item introduction over {\tt ->} (respectively {\tt <-}) expects the
+  hypothesis to be an equality and the right-hand-side (respectively
+  the left-hand-side) is replaced by the left-hand-side (respectively
+  the right-hand-side) in both the conclusion and the context of the goal;
+  if moreover the term to substitute is a variable, the hypothesis is
+  removed.
 \end{itemize}
 
-\Rem The pattern {\tt ($p_1$, {\ldots}, $p_n$)}
-is a synonym for the pattern {\tt [$p_1$ {\ldots} $p_n$]}, i.e. it
-corresponds to the decomposition of an hypothesis typed by an
-inductive type with a single constructor.
+\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros
+  $p_1$;\ldots; intros $p_n$} for the following reasons:
+\begin{itemize}
+\item A wildcard pattern never succeeds when applied isolated on a
+  dependent product, while it succeeds as part of a list of
+  introduction patterns if the hypotheses that depends on it are
+  erased too.
+\item A disjunctive or conjunctive pattern followed by an introduction
+  pattern forces the introduction in the context of all arguments of
+  the constructors before applying the next pattern while a terminal
+  disjunctive or conjunctive pattern does not. Here is an example
+
+\begin{coq_example}
+Goal forall n:nat, n = 0 -> n = 0.
+intros [ | ] H.
+Show 2.
+Undo.
+intros [ | ]; intros H.
+Show 2.
+\end{coq_example}
+
+\end{itemize}
 
 \Rem An additional abbreviation is allowed for sequences of rightmost
-binary conjonctions: pattern 
+binary conjunctions: pattern 
 {\tt \{} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt \}} 
 is a synonym for pattern 
 {\tt (} $p_1$ {\tt , (} $p_2$ {\tt ,} {\ldots} {\tt (}$p_{n-1}${\tt ,}$p_n${\tt )} {\ldots}  {\tt ))}.
-In particular it can be used to introduce existential hypothesis
-and/or n-ary conjonctions. 
-
+In particular it can be used to introduce existential hypotheses
+and/or n-ary conjunctions. 
 
 \begin{coq_example}
 Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
@@ -1574,7 +1706,7 @@ this tactic. The tactic is based on the BasicElim tactic by Conor
 McBride \cite{DBLP:conf/types/McBride00} and the work of Cristina Cornes
 around inversion \cite{DBLP:conf/types/CornesT95}. From an instantiated
 inductive predicate and a goal it generates an equivalent goal where the
-hypothesis has been generalised over its indices which are then
+hypothesis has been generalized over its indexes which are then
 constrained by equalities to be the right instances. This permits to
 state lemmas without resorting to manually adding these equalities and
 still get enough information in the proofs. 
@@ -1588,7 +1720,7 @@ Lemma le_minus : forall n:nat, n < 1 -> n = 0.
 intros n H ; induction H.
 \end{coq_example}
 
-Here we didn't get any information on the indices to help fullfill this
+Here we didn't get any information on the indexes to help fulfill this
 proof. The problem is that when we use the \texttt{induction} tactic
 we lose information on the hypothesis instance, notably that the second
 argument is \texttt{1} here. Dependent induction solves this problem by
@@ -1814,10 +1946,10 @@ This happens if \term$_1$ does not occur in the goal.
     \texttt{H1} instead of the current goal.
   \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1;
       rewrite H in H2}. In particular a failure will happen if any of
-    these three simplier tactics fails. 
+    these three simpler tactics fails. 
   \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
       H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
-    as soon as at least one of these simplier tactics succeeds.
+    as soon as at least one of these simpler tactics succeeds.
   \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} 
     and \texttt{rewrite H in * |-} that succeeds if at
     least one of these two tactics succeeds. 
@@ -1892,7 +2024,7 @@ n}| assumption || symmetry; try assumption]}.
     {\tt replace -> {\term} \textit{clause}}\\ 
     {\tt replace -> {\term} \textit{clause}}\\ 
     Act as before but the replacements take place in \textit{clause}~\ref{Conversion-tactics} an not only in the conclusion of the goal.\\
-    The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
+    The  \textit{clause} argument must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
 \end{Variants}
 
 \subsection{\tt reflexivity
@@ -2197,7 +2329,7 @@ If the current goal has form $\verb=~=t_1=t_2$, then this tactic does
 \label{dependent-rewrite}}
 
 This tactic applies to any goal.  If \ident\ has type 
-\verb+(existS A B a b)=(existS A B a' b')+ 
+\verb+(existT B a b)=(existT B a' b')+ 
 in the local context (i.e. each term of the
 equality has a sigma type $\{ a:A~ \&~(B~a)\}$) this tactic rewrites
 \verb+a+ into \verb+a'+ and \verb+b+ into \verb+b'+ in the current
@@ -2554,7 +2686,7 @@ hints of the database named {\tt core}.
 
 \item \texttt{auto using $lemma_1, \ldots, lemma_n$}
 
-  Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be conbined
+  Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be combined
   with the \texttt{with \ident} option).
 
 \item {\tt trivial}\tacindex{trivial}
@@ -2691,7 +2823,7 @@ internally replaces it by the equivalent one:
 and then uses {\tt auto} which completes the proof.
 
 Originally due to C{\'e}sar~Mu{\~n}oz, these tactics ({\tt tauto} and {\tt intuition})
-have been completely reengineered by David~Delahaye using mainly the tactic
+have been completely re-engineered by David~Delahaye using mainly the tactic
 language (see Chapter~\ref{TacticLanguage}). The code is now quite shorter and
 a significant increase in performances has been noticed. The general behavior
 with respect to dependent types, unfolding and introductions has
@@ -2870,7 +3002,7 @@ If the goal is a non-quantified equality, {\tt congruence} tries to
 prove it with non-quantified equalities in the context. Otherwise it
 tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis.
 
-{\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the memebers of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. 
+{\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. 
 
 \begin{coq_eval}
 Reset Initial.
@@ -2902,7 +3034,7 @@ congruence.
 
 \begin{Variants}
  \item {\tt congruence {\sl n}}\\
-  Tries to add at most {\tt \sl n} instances of hypotheses satting quantifiesd equalities to the problem in order to solve it. A bigger value of {\tt \sl n} does not make success slower, only failure. You might consider adding some lemmata as hypotheses using {\tt assert} in order for congruence to use them.
+  Tries to add at most {\tt \sl n} instances of hypotheses stating quantified equalities to the problem in order to solve it. A bigger value of {\tt \sl n} does not make success slower, only failure. You might consider adding some lemmas as hypotheses using {\tt assert} in order for congruence to use them.
 
 \end{Variants}
 
@@ -2916,7 +3048,7 @@ congruence.
 \begin{ErrMsgs}
   \item \errindex{I don't know how to handle dependent equality} \\
     The decision procedure managed to find a proof of the goal or of
-    a discriminable equality but this proof couldn't be built in Coq
+    a discriminable equality but this proof couldn't be built in {\Coq}
     because of dependently-typed functions.
   \item \errindex{I couldn't solve goal} \\
     The decision procedure didn't find any way to solve the goal.
@@ -2938,7 +3070,7 @@ The tactic \texttt{omega}, due to Pierre Cr{\'e}gut,
 is an automatic decision procedure for Presburger
 arithmetic. It solves quantifier-free 
 formulas built with \verb|~|, \verb|\/|, \verb|/\|,
-\verb|->| on top of equalities and inequalities on
+\verb|->| on top of equalities, inequalities and disequalities on
 both the type \texttt{nat} of natural numbers and \texttt{Z} of binary
 integers. This tactic must be loaded by the command \texttt{Require Import
   Omega}. See the additional documentation about \texttt{omega}
@@ -2979,7 +3111,7 @@ operations) to a fraction made of two polynomial expressions.
 
 Tactic {\tt field} is used to solve subgoals, whereas {\tt
   field\_simplify \term$_1$\dots\term$_n$} replaces the provided terms
-by their reducted fraction. {\tt field\_simplify\_eq} applies when the
+by their reduced fraction. {\tt field\_simplify\_eq} applies when the
 conclusion is an equation: it simplifies both hand sides and multiplies
 so as to cancel denominators. So it produces an equation without
 division nor inverse.
@@ -3014,7 +3146,7 @@ field}.
 \subsection{\tt fourier
 \tacindex{fourier}}
 
-This tactic written by Lo{\"\i}c Pottier solves linear inequations on
+This tactic written by Lo{\"\i}c Pottier solves linear inequalities on
 real numbers using Fourier's method~\cite{Fourier}. This tactic must
 be loaded by {\tt Require Import Fourier}.
 
@@ -3040,7 +3172,7 @@ Reset Initial.
 This tactic \footnote{The behavior of this tactic has much changed compared to
 the versions available in the previous distributions (V6). This may cause
 significant changes in your theories to obtain the same result. As a drawback
-of the reengineering of the code, this tactic has also been completely revised
+of the re-engineering of the code, this tactic has also been completely revised
 to get a very compact and readable version.} carries out rewritings according
 the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}.
 
@@ -3058,7 +3190,7 @@ command.
 
 \begin{Variant}
 \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
-Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
+Performs, in the same way, all the rewritings of the bases {\tt \ident$_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
 
 \item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
@@ -3071,7 +3203,7 @@ $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
 
 \item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in \textit{clause}}
   Performs all  the rewritings  in the clause \textit{clause}. \\
-  The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
+  The  \textit{clause} argument must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
 
 \end{Variant}
 
@@ -3317,20 +3449,20 @@ databases are non empty and can be used.
   from the \texttt{Init} and \texttt{Logic} directories.
 
 \item[\tt arith] This database contains all lemmas about Peano's
-  arithmetic proven in the directories \texttt{Init} and
+  arithmetic proved in the directories \texttt{Init} and
   \texttt{Arith}
 
 \item[\tt zarith] contains lemmas about binary signed integers from
   the directories \texttt{theories/ZArith}. When required, the module
   {\tt Omega} also extends the database {\tt zarith} with a high-cost
-  hint that calls {\tt omega} on equations and inequations in {\tt
+  hint that calls {\tt omega} on equations and inequalities in {\tt
   nat} or {\tt Z}.
 
 \item[\tt bool] contains lemmas about booleans, mostly from directory
   \texttt{theories/Bool}.
 
 \item[\tt datatypes] is for lemmas about lists, streams and so on that 
-  are mainly proven in the \texttt{Lists} subdirectory.
+  are mainly proved in the \texttt{Lists} subdirectory.
 
 \item[\tt sets] contains lemmas about sets and relations from the 
   directories \texttt{Sets} and \texttt{Relations}.
@@ -3340,7 +3472,7 @@ There is also a special database called {\tt v62}. It collects all
 hints that were declared in the versions of {\Coq} prior to version
 6.2.4 when the databases {\tt core}, {\tt arith}, and so on were
 introduced.  The purpose of the database {\tt v62} is to ensure
-compatibility with further versions of Coq for developments done in
+compatibility with further versions of {\Coq} for developments done in
 versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}).
 The database {\tt v62} is intended not to be extended (!). It is not
 included in the hint databases list used in the {\tt auto with *} tactic.
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0e30e5db5..1e3587c59 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -922,7 +922,7 @@ let rec raw_of_pat env = function
 	| Name id   -> id
 	| Anonymous ->
 	    anomaly "rawconstr_of_pattern: index to an anonymous variable"
-      with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in
+      with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)^"]") in
       RVar (loc,id)
   | PMeta None -> RHole (loc,Evd.InternalHole)
   | PMeta (Some n) -> RPatVar (loc,(false,n))
diff --git a/kernel/names.ml b/kernel/names.ml
index 46a44a9b2..125c9b6de 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -17,7 +17,7 @@ type identifier = string
 
 let id_ord = Pervasives.compare
 
-let id_of_string s = String.copy s
+let id_of_string s = check_ident s; String.copy s
 
 let string_of_id id = String.copy id
 
@@ -185,7 +185,7 @@ module Cmap = KNmap
 module Cpred = KNpred
 module Cset = KNset
 
-let default_module_name = id_of_string "If you see this, it's a bug"
+let default_module_name = "If you see this, it's a bug"
 
 let initial_dir = make_dirpath [default_module_name]
 
diff --git a/lib/util.ml b/lib/util.ml
index ce336ac34..b317c849c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -50,15 +50,8 @@ let pi3 (_,_,a) = a
 
 (* Characters *)
 
-let is_letter c =
-  (c >= 'a' && c <= 'z') or
-  (c >= 'A' && c <= 'Z') or
-  (c >= '\248' && c <= '\255') or
-  (c >= '\192' && c <= '\214') or
-  (c >= '\216' && c <= '\246')
-
+let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
 let is_digit c = (c >= '0' && c <= '9')
-
 let is_ident_tail c =
   is_letter c or is_digit c or c = '\'' or c = '_'
 
@@ -126,6 +119,179 @@ module Stringset = Set.Make(struct type t = string let compare = compare end)
 
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
+type utf8_status = Utf8Letter | Utf8IdentPart | Utf8Symbol
+
+exception UnsupportedUtf8
+
+let classify_utf8 unicode =
+    match unicode land 0x1F000 with
+    | 0x0 ->
+    begin match unicode with
+    (* utf-8 Basic Latin underscore *)
+    | x when x = 0x005F -> Utf8Letter
+    (* utf-8 Basic Latin letters *)
+    | x when 0x0041 <= x & x <= 0x005A -> Utf8Letter
+    | x when 0x0061 <= x & x <= 0x007A -> Utf8Letter
+    (* utf-8 Basic Latin digits and quote *)
+    | x when 0x0030 <= x & x <= 0x0039 or x = 0x0027 -> Utf8IdentPart
+    (* utf-8 Basic Latin symbols *)
+    | x when x <= 0x007F -> Utf8Symbol
+    (* utf-8 Latin-1 non breaking space U00A0 *)
+    | 0x00A0 -> Utf8Letter
+    (* utf-8 Latin-1 symbols U00A1-00BF *)
+    | x when 0x00A0 <= x & x <= 0x00BF -> Utf8Symbol
+    (* utf-8 Latin-1 letters U00C0-00D6 *)
+    | x when 0x00C0 <= x & x <= 0x00D6 -> Utf8Letter
+    (* utf-8 Latin-1 symbol U00D7 *)
+    | 0x00D7 -> Utf8Symbol
+    (* utf-8 Latin-1 letters U00D8-00F6 *)
+    | x when 0x00D8 <= x & x <= 0x00F6 -> Utf8Letter
+    (* utf-8 Latin-1 symbol U00F7 *)
+    | 0x00F7 -> Utf8Symbol
+    (* utf-8 Latin-1 letters U00F8-00FF *)
+    | x when 0x00F8 <= x & x <= 0x00FF -> Utf8Letter
+    (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *)
+    | x when 0x0100 <= x & x <= 0x0241 -> Utf8Letter
+    (* utf-8 Phonetic letters U0250-02AF *)
+    | x when 0x0250 <= x & x <= 0x02AF -> Utf8Letter
+    (* utf-8 what do to with diacritics U0300-U036F ? *)
+    (* utf-8 Greek letters U0380-03FF *)
+    | x when 0x0380 <= x & x <= 0x03FF -> Utf8Letter
+    (* utf-8 Cyrillic letters U0400-0481 *)
+    | x when 0x0400 <= x & x <= 0x0481 -> Utf8Letter
+    (* utf-8 Cyrillic symbol U0482 *)
+    | 0x0482 -> Utf8Symbol
+    (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *)
+    (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
+    | x when 0x048A <= x & x <= 0x04F9 -> Utf8Letter
+    (* utf-8 Cyrillic supplement letters U0500-U050F *)
+    | x when 0x0500 <= x & x <= 0x050F -> Utf8Letter
+    (* utf-8 Hebrew letters U05D0-05EA *)
+    | x when 0x05D0 <= x & x <= 0x05EA -> Utf8Letter
+    (* utf-8 Arabic letters U0621-064A *)
+    | x when 0x0621 <= x & x <= 0x064A -> Utf8Letter
+    (* utf-8 Arabic supplement letters U0750-076D *)
+    | x when 0x0750 <= x & x <= 0x076D -> Utf8Letter
+    | _ -> raise UnsupportedUtf8
+    end
+    | 0x1000 ->
+    begin match unicode with
+    (* utf-8 Georgian U10A0-10FF (has holes) *)
+    | x when 0x10A0 <= x & x <= 0x10FF -> Utf8Letter
+    (* utf-8 Hangul Jamo U1100-11FF (has holes) *)
+    | x when 0x1100 <= x & x <= 0x11FF -> Utf8Letter
+    (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *)
+    | x when 0x1E00 <= x & x <= 0x1E9B -> Utf8Letter
+    | x when 0x1EA0 <= x & x <= 0x1EF9 -> Utf8Letter
+    | _ -> raise UnsupportedUtf8
+    end
+    | 0x2000 ->
+    begin match unicode with
+    (* utf-8 general punctuation U2080-2089 *)
+    (* Hyphens *)
+    | x when 0x2010 <= x & x <= 0x2011 -> Utf8Letter 
+    (* Dashes and other symbols *)
+    | x when 0x2012 <= x & x <= 0x2027 -> Utf8Symbol
+    (* Per mille and per ten thousand signs *)
+    | x when 0x2030 <= x & x <= 0x2031 -> Utf8Symbol
+    (* Prime letters *)
+    | x when 0x2032 <= x & x <= 0x2034 or x = 0x2057 -> Utf8IdentPart
+    (* Miscellaneous punctuation *)
+    | x when 0x2039 <= x & x <= 0x2056 -> Utf8Symbol
+    | x when 0x2058 <= x & x <= 0x205E -> Utf8Symbol
+    (* Invisible mathematical operators *)
+    | x when 0x2061 <= x & x <= 0x2063 -> Utf8Symbol
+    (* utf-8 superscript U2070-207C *) 
+    | x when 0x2070 <= x & x <= 0x207C -> Utf8Symbol
+    (* utf-8 subscript U2080-2089 *) 
+    | x when 0x2080 <= x & x <= 0x2089 -> Utf8IdentPart
+    (* utf-8 letter-like U2100-214F *)
+    | x when 0x2100 <= x & x <= 0x214F -> Utf8Letter
+    (* utf-8 number-forms U2153-2183 *)
+    | x when 0x2153 <= x & x <= 0x2183 -> Utf8Symbol
+    (* utf-8 arrows A U2190-21FF *)
+    (* utf-8 mathematical operators U2200-22FF *)
+    (* utf-8 miscellaneous technical U2300-23FF *)
+    | x when 0x2190 <= x & x <= 0x23FF -> Utf8Symbol
+    (* utf-8 box drawing U2500-257F has ceiling, etc. *)
+    (* utf-8 block elements U2580-259F *)
+    (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *)
+    (* utf-8 miscellaneous symbols U2600-26FF *)
+    | x when 0x2500 <= x & x <= 0x26FF -> Utf8Symbol
+    (* utf-8 arrows B U2900-297F *)
+    | x when 0x2900 <= x & x <= 0x297F -> Utf8Symbol
+    (* utf-8 mathematical operators U2A00-2AFF *)
+    | x when 0x2A00 <= x & x <= 0x2AFF -> Utf8Symbol
+    (* utf-8 bold symbols U2768-U2775 *)
+    | x when 0x2768 <= x & x <= 0x2775 -> Utf8Symbol
+    (* utf-8 arrows and brackets U27E0-U27FF *)
+    | x when 0x27E0 <= x & x <= 0x27FF -> Utf8Symbol
+    (* utf-8 brackets, braces and parentheses *)
+    | x when 0x2980 <= x & x <= 0x299F -> Utf8Symbol
+    (* utf-8 miscellaneous including double-plus U29F0-U29FF *)
+    | x when 0x29F0 <= x & x <= 0x29FF -> Utf8Symbol
+    | _ -> raise UnsupportedUtf8
+    end
+    | _ ->
+    begin match unicode with
+    (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *)
+    | x when 0x3040 <= x & x <= 0x30FF -> Utf8Letter
+    (* utf-8 Unified CJK Ideographs U4E00-9FA5 *)
+    | x when 0x4E00 <= x & x <= 0x9FA5 -> Utf8Letter
+    (* utf-8 Hangul syllables UAC00-D7AF *)
+    | x when 0xAC00 <= x & x <= 0xD7AF -> Utf8Letter
+    (* utf-8 Gothic U10330-1034A *)
+    | x when 0x10330 <= x & x <= 0x1034A -> Utf8Letter
+    | _ -> raise UnsupportedUtf8
+    end
+
+exception End_of_input
+
+let next_utf8 s i =
+  let err () = invalid_arg "utf8" in
+  let l = String.length s - i in
+  if l = 0 then raise End_of_input
+  else let a = Char.code s.[i] in if a <= 0x7F then
+    1, a
+  else if a land 0x40 = 0 then err ()
+  else if l = 1 then err ()
+  else let b = Char.code s.[i+1] in if b land 0xC0 <> 0x80 then err ()
+  else if a land 0x20 = 0 then
+    2, (a land 0x1F) lsl 6 + (b land 0x3F)
+  else if l = 2 then err ()
+  else let c = Char.code s.[i+2] in if c land 0xC0 <> 0x80 then err ()
+  else if a land 0x10 = 0 then
+    3, (a land 0x0F) lsl 12 + (b land 0x3F) lsl 6 + (c land 0x3F)
+  else if l = 3 then err ()
+  else let d = Char.code s.[i+3] in if d land 0xC0 <> 0x80 then err ()
+  else if a land 0x08 = 0 then
+    4, (a land 0x07) lsl 18 + (b land 0x3F) lsl 12 +
+       (c land 0x3F) lsl 6 + (d land 0x3F)
+  else err ()
+
+(* Check the well-formedness of an identifier *)
+
+let check_ident s =
+  let i = ref 0 in
+  if s <> ".." then try
+    let j, n = next_utf8 s 0 in
+    match classify_utf8 n with
+    | Utf8Letter ->
+	i := !i + j;
+	begin try
+	  while true do
+	    let j, n = next_utf8 s !i in
+	    match classify_utf8 n with
+	    | Utf8Letter | Utf8IdentPart -> i := !i + j
+	    | _ -> error
+		("invalid character "^(String.sub s !i j)^" in identifier "^s)
+	  done
+	with End_of_input -> () end
+    | _ -> error (s^": an identifier should start with a letter")
+  with 
+  | End_of_input -> error "The empty string is not an identifier"
+  | Invalid_argument _ -> error (s^": invalid utf8 sequence")
+
 (* Lists *)
 
 let list_intersect l1 l2 = 
diff --git a/lib/util.mli b/lib/util.mli
index befe844bc..bcaa08b2e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -78,6 +78,13 @@ val parse_loadpath : string -> string list
 module Stringset : Set.S with type elt = string
 module Stringmap : Map.S with type key = string
 
+type utf8_status = Utf8Letter | Utf8IdentPart | Utf8Symbol
+
+exception UnsupportedUtf8
+
+val classify_utf8 : int -> utf8_status
+val check_ident : string -> unit
+
 (*s Lists. *)
 
 val list_add_set : 'a -> 'a list -> 'a list
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index b2c279b39..a477e3fd4 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -73,7 +73,7 @@ let make_constr_action
 	  make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:constr_expr list) ->
-          let dummyid = Ident (dummy_loc,id_of_string "") in
+          let dummyid = Ident (dummy_loc,id_of_string "_") in
 	  make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
     | Some (p, ETPattern) :: tl -> 
 	failwith "Unexpected entry of type cases pattern" in
@@ -99,7 +99,7 @@ let make_cases_pattern_action
 	  make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:cases_pattern_expr list) ->
-          let dummyid = Ident (dummy_loc,id_of_string "") in
+          let dummyid = Ident (dummy_loc,id_of_string "_") in
 	  make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
     | Some (p, (ETPattern | ETOther _)) :: tl -> 
 	failwith "Unexpected entry of type cases pattern or other" in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 522022bb3..28c2acb81 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -470,14 +470,22 @@ GEXTEND Gram
       | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
 
       (* Constructors *)
-      | IDENT "left"; bl = with_bindings -> TacLeft bl
-      | IDENT "right"; bl = with_bindings -> TacRight bl
-      | IDENT "split"; bl = with_bindings -> TacSplit (false,bl)
-      | "exists"; bl = bindings -> TacSplit (true,bl)
-      | "exists" -> TacSplit (true,NoBindings)
+      | IDENT "left";   bl = with_bindings -> TacLeft  (false,bl)
+      | IDENT "eleft";  bl = with_bindings -> TacLeft  (true,bl)
+      | IDENT "right";  bl = with_bindings -> TacRight (false,bl)
+      | IDENT "eright"; bl = with_bindings -> TacRight (true,bl)
+      | IDENT "split";  bl = with_bindings -> TacSplit (false,false,bl)
+      | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,bl)
+      | "exists";       bl = bindings -> TacSplit (false,true,bl)
+      | "eexists";      bl = bindings -> TacSplit (true,true,bl)
+      | "exists"  (* meaningless? *)  -> TacSplit (false,true,NoBindings)
+      | "eexists"                     -> TacSplit (true,true,NoBindings)
       | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
-	  TacConstructor (n,l)
-      | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor t
+	  TacConstructor (false,n,l)
+      | IDENT "econstructor"; n = num_or_meta; l = with_bindings ->
+	  TacConstructor (true,n,l)
+      | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor (false,t)
+      | IDENT "econstructor"; t = OPT tactic -> TacAnyConstructor (true,t)
 
       (* Equivalence relations *)
       | IDENT "reflexivity" -> TacReflexivity
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 800dc6a03..5d59a8489 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -14,6 +14,7 @@
  * ast-based camlp4 *)
 
 open Pp
+open Util
 open Token
 
 (* Dictionaries: trees annotated with string options, each node being a map
@@ -76,8 +77,10 @@ let bad_token str = raise (Error (Bad_token str))
 
 (* Lexer conventions on tokens *)
 
-type utf8_token =
-    Utf8Letter of int | Utf8IdentPart of int | Utf8Symbol | AsciiChar
+type token_kind =
+  | Utf8Token of (utf8_status * int)
+  | AsciiChar
+  | EmptyStream
 
 let error_unsupported_unicode_character n cs =
   let bp = Stream.count cs in
@@ -121,123 +124,14 @@ let lookup_utf8_tail c cs =
 	  (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F)
       | _ -> error_utf8 cs
     in
-    match unicode land 0x1F000 with
-    | 0x0 ->
-    begin match unicode with
-    (* utf-8 Latin-1 non breaking space U00A0 *)
-    | 0x00A0 -> Utf8Letter n
-    (* utf-8 Latin-1 symbols U00A1-00BF *)
-    | x when 0x00A0 <= x & x <= 0x00BF -> Utf8Symbol
-    (* utf-8 Latin-1 letters U00C0-00D6 *)
-    | x when 0x00C0 <= x & x <= 0x00D6 -> Utf8Letter n
-    (* utf-8 Latin-1 symbol U00D7 *)
-    | 0x00D7 -> Utf8Symbol
-    (* utf-8 Latin-1 letters U00D8-00F6 *)
-    | x when 0x00D8 <= x & x <= 0x00F6 -> Utf8Letter n
-    (* utf-8 Latin-1 symbol U00F7 *)
-    | 0x00F7 -> Utf8Symbol
-    (* utf-8 Latin-1 letters U00F8-00FF *)
-    | x when 0x00F8 <= x & x <= 0x00FF -> Utf8Letter n
-    (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *)
-    | x when 0x0100 <= x & x <= 0x0241 -> Utf8Letter n
-    (* utf-8 Phonetic letters U0250-02AF *)
-    | x when 0x0250 <= x & x <= 0x02AF -> Utf8Letter n
-    (* utf-8 what do to with diacritics U0300-U036F ? *)
-    (* utf-8 Greek letters U0380-03FF *)
-    | x when 0x0380 <= x & x <= 0x03FF -> Utf8Letter n
-    (* utf-8 Cyrillic letters U0400-0481 *)
-    | x when 0x0400 <= x & x <= 0x0481 -> Utf8Letter n
-    (* utf-8 Cyrillic symbol U0482 *)
-    | 0x0482 -> Utf8Symbol
-    (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *)
-    (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
-    | x when 0x048A <= x & x <= 0x04F9 -> Utf8Letter n
-    (* utf-8 Cyrillic supplement letters U0500-U050F *)
-    | x when 0x0500 <= x & x <= 0x050F -> Utf8Letter n
-    (* utf-8 Hebrew letters U05D0-05EA *)
-    | x when 0x05D0 <= x & x <= 0x05EA -> Utf8Letter n
-    (* utf-8 Arabic letters U0621-064A *)
-    | x when 0x0621 <= x & x <= 0x064A -> Utf8Letter n
-    (* utf-8 Arabic supplement letters U0750-076D *)
-    | x when 0x0750 <= x & x <= 0x076D -> Utf8Letter n
-    | _ -> error_unsupported_unicode_character n cs
-    end
-    | 0x1000 ->
-    begin match unicode with
-    (* utf-8 Georgian U10A0-10FF (has holes) *)
-    | x when 0x10A0 <= x & x <= 0x10FF -> Utf8Letter n
-    (* utf-8 Hangul Jamo U1100-11FF (has holes) *)
-    | x when 0x1100 <= x & x <= 0x11FF -> Utf8Letter n
-    (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *)
-    | x when 0x1E00 <= x & x <= 0x1E9B -> Utf8Letter n
-    | x when 0x1EA0 <= x & x <= 0x1EF9 -> Utf8Letter n
-    | _ -> error_unsupported_unicode_character n cs
-    end
-    | 0x2000 ->
-    begin match unicode with
-    (* utf-8 general punctuation U2080-2089 *)
-    (* Hyphens *)
-    | x when 0x2010 <= x & x <= 0x2011 -> Utf8Letter n 
-    (* Dashes and other symbols *)
-    | x when 0x2012 <= x & x <= 0x2027 -> Utf8Symbol
-    (* Per mille and per ten thousand signs *)
-    | x when 0x2030 <= x & x <= 0x2031 -> Utf8Symbol
-    (* Prime letters *)
-    | x when 0x2032 <= x & x <= 0x2034 or x = 0x2057 -> Utf8IdentPart n
-    (* Miscellaneous punctuation *)
-    | x when 0x2039 <= x & x <= 0x2056 -> Utf8Symbol
-    | x when 0x2058 <= x & x <= 0x205E -> Utf8Symbol
-    (* Invisible mathematical operators *)
-    | x when 0x2061 <= x & x <= 0x2063 -> Utf8Symbol
-    (* utf-8 superscript U2070-207C *) 
-    | x when 0x2070 <= x & x <= 0x207C -> Utf8Symbol
-    (* utf-8 subscript U2080-2089 *) 
-    | x when 0x2080 <= x & x <= 0x2089 -> Utf8IdentPart n
-    (* utf-8 letter-like U2100-214F *)
-    | x when 0x2100 <= x & x <= 0x214F -> Utf8Letter n
-    (* utf-8 number-forms U2153-2183 *)
-    | x when 0x2153 <= x & x <= 0x2183 -> Utf8Symbol
-    (* utf-8 arrows A U2190-21FF *)
-    (* utf-8 mathematical operators U2200-22FF *)
-    (* utf-8 miscellaneous technical U2300-23FF *)
-    | x when 0x2190 <= x & x <= 0x23FF -> Utf8Symbol
-    (* utf-8 box drawing U2500-257F has ceiling, etc. *)
-    (* utf-8 block elements U2580-259F *)
-    (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *)
-    (* utf-8 miscellaneous symbols U2600-26FF *)
-    | x when 0x2500 <= x & x <= 0x26FF -> Utf8Symbol
-    (* utf-8 arrows B U2900-297F *)
-    | x when 0x2900 <= x & x <= 0x297F -> Utf8Symbol
-    (* utf-8 mathematical operators U2A00-2AFF *)
-    | x when 0x2A00 <= x & x <= 0x2AFF -> Utf8Symbol
-    (* utf-8 bold symbols U2768-U2775 *)
-    | x when 0x2768 <= x & x <= 0x2775 -> Utf8Symbol
-    (* utf-8 arrows and brackets U27E0-U27FF *)
-    | x when 0x27E0 <= x & x <= 0x27FF -> Utf8Symbol
-    (* utf-8 brackets, braces and parentheses *)
-    | x when 0x2980 <= x & x <= 0x299F -> Utf8Symbol
-    (* utf-8 miscellaneous including double-plus U29F0-U29FF *)
-    | x when 0x29F0 <= x & x <= 0x29FF -> Utf8Symbol
-    | _ -> error_unsupported_unicode_character n cs
-    end
-    | _ ->
-    begin match unicode with
-    (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *)
-    | x when 0x3040 <= x & x <= 0x30FF -> Utf8Letter n
-    (* utf-8 Unified CJK Ideographs U4E00-9FA5 *)
-    | x when 0x4E00 <= x & x <= 0x9FA5 -> Utf8Letter n
-    (* utf-8 Hangul syllables UAC00-D7AF *)
-    | x when 0xAC00 <= x & x <= 0xD7AF -> Utf8Letter n
-    (* utf-8 Gothic U10330-1034A *)
-    | x when 0x10330 <= x & x <= 0x1034A -> Utf8Letter n
-    | _ -> error_unsupported_unicode_character n cs
-    end
+    try classify_utf8 unicode, n
+    with UnsupportedUtf8 -> error_unsupported_unicode_character n cs
 	
 let lookup_utf8 cs =
   match Stream.peek cs with
-    | Some ('\x00'..'\x7F') -> Some AsciiChar
-    | Some ('\x80'..'\xFF' as c) -> Some (lookup_utf8_tail c cs)
-    | None -> None
+    | Some ('\x00'..'\x7F') -> AsciiChar
+    | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs)
+    | None -> EmptyStream
 
 let check_special_token str =
   let rec loop_symb = parser
@@ -249,16 +143,16 @@ let check_special_token str =
 
 let check_ident str =
   let rec loop_id intail = parser
-    | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '_'); s >] ->
+    | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] ->
         loop_id true s
     | [< ' ('0'..'9' | ''') when intail; s >] ->
         loop_id true s
     | [< s >] ->
 	match lookup_utf8 s with
-	| Some (Utf8Letter n) -> njunk n s; loop_id true s
-	| Some (Utf8IdentPart n) when intail -> njunk n s; loop_id true s
-	| Some _ -> bad_token str
-	| None -> ()
+	| Utf8Token (Utf8Letter, n) -> njunk n s; loop_id true s
+	| Utf8Token (Utf8IdentPart, n) when intail -> njunk n s; loop_id true s
+	| EmptyStream -> ()
+	| Utf8Token _ | AsciiChar -> bad_token str
   in
   loop_id false (Stream.of_string str)
 
@@ -323,7 +217,7 @@ let rec ident_tail len = parser
       ident_tail (store len c) s
   | [< s >] ->
       match lookup_utf8 s with
-      | Some (Utf8IdentPart n | Utf8Letter n) ->
+      | Utf8Token ((Utf8IdentPart | Utf8Letter), n) ->
 	  ident_tail (nstore n len s) s
       | _ -> len
 
@@ -480,9 +374,9 @@ let parse_after_dot bp c =
       (constructor, get_buff len)
   | [< s >] ->
       match lookup_utf8 s with
-      | Some (Utf8Letter n) -> 
+      | Utf8Token (Utf8Letter, n) -> 
 	  (constructor, get_buff (ident_tail (nstore n 0 s) s))
-      | Some (Utf8IdentPart _ | AsciiChar | Utf8Symbol) | None -> 
+      | AsciiChar | Utf8Token _ | EmptyStream -> 
 	  fst (process_chars bp c s)
 
 (* Parse a token in a char stream *)
@@ -518,16 +412,16 @@ let rec next_token = parser bp
       t
   | [< s >] ->
       match lookup_utf8 s with
-	| Some (Utf8Letter n) ->
+	| Utf8Token (Utf8Letter, n) ->
 	    let len = ident_tail (nstore n 0 s) s in
 	    let id = get_buff len in
 	    let ep = Stream.count s in
 	    comment_stop bp;
 	    (try ("",find_keyword id) with Not_found -> ("IDENT",id)), (bp, ep)
-	| Some (Utf8Symbol | AsciiChar | Utf8IdentPart _) -> 
+	| AsciiChar | Utf8Token ((Utf8Symbol | Utf8IdentPart), _) -> 
 	    let t = process_chars bp (Stream.next s) s in
 	    comment_stop bp; t
-	| None ->
+	| EmptyStream ->
 	    comment_stop bp; (("EOI", ""), (bp, bp + 1))
 
 (* Location table system for creating tables associating a token count
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d4a809756..55c6a4387 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -133,6 +133,8 @@ let rec pr_message_token prid = function
 
 let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
 
+let with_evars ev s = if ev then "e" ^ s else s
+
 let out_bindings = function
   | ImplicitBindings l -> ImplicitBindings (List.map snd l)
   | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l)
@@ -637,7 +639,8 @@ let rec pr_atom0 = function
   | TacIntroPattern [] -> str "intros"
   | TacIntroMove (None,None) -> str "intro"
   | TacAssumption -> str "assumption"
-  | TacAnyConstructor None -> str "constructor"
+  | TacAnyConstructor (false,None) -> str "constructor"
+  | TacAnyConstructor (true,None) -> str "econstructor"
   | TacTrivial ([],Some []) -> str "trivial"
   | TacAuto (None,[],Some []) -> str "auto"
   | TacReflexivity -> str "reflexivity"
@@ -674,14 +677,14 @@ and pr_atom1 = function
   | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
   | TacApply (a,ev,cb) ->
       hov 1 ((if a then mt() else str "simple ") ++
-             str (if ev then "eapply" else "apply") ++ spc () ++ 
+             str (with_evars ev "apply") ++ spc () ++ 
              pr_with_bindings cb)
   | TacElim (ev,cb,cbo) ->
-      hov 1 (str (if ev then "eelim" else "elim") ++ pr_arg pr_with_bindings cb ++ 
+      hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ 
         pr_opt pr_eliminator cbo)
   | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c)
   | TacCase (ev,cb) ->
-      hov 1 (str (if ev then "ecase" else "case") ++ spc () ++ pr_with_bindings cb)
+      hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
   | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
@@ -724,14 +727,14 @@ and pr_atom1 = function
   | TacSimpleInduction h ->
       hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewInduction (ev,h,e,ids) ->
-      hov 1 (str (if ev then "einduction" else "induction") ++ spc () ++
+      hov 1 (str (with_evars ev "induction") ++ spc () ++
 	     prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
 	     pr_with_names ids ++
              pr_opt pr_eliminator e)
   | TacSimpleDestruct h ->
       hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewDestruct (ev,h,e,ids) ->
-      hov 1 (str (if ev then "edestruct" else "destruct") ++ spc () ++
+      hov 1 (str (with_evars ev "destruct") ++ spc () ++
              prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ 
 	     pr_with_names ids ++
              pr_opt pr_eliminator e)
@@ -792,15 +795,16 @@ and pr_atom1 = function
       hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) 
 
   (* Constructors *)
-  | TacLeft l -> hov 1 (str "left" ++ pr_bindings l)
-  | TacRight l -> hov 1 (str "right" ++ pr_bindings l)
-  | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings l)
-  | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings l)
-  | TacAnyConstructor (Some t) ->
-      hov 1 (str "constructor" ++ pr_arg (pr_tac_level (latom,E)) t)
-  | TacAnyConstructor None as t -> pr_atom0 t
-  | TacConstructor (n,l) ->
-      hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l)
+  | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l)
+  | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l)
+  | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ pr_bindings l)
+  | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ pr_ex_bindings l)
+  | TacAnyConstructor (ev,Some t) ->
+      hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t)
+  | TacAnyConstructor (ev,None) as t -> pr_atom0 t
+  | TacConstructor (ev,n,l) ->
+      hov 1 (str (with_evars ev "constructor") ++ 
+             pr_or_metaid pr_intarg n ++ pr_bindings l)
 
   (* Conversion *)  
   | TacReduce (r,h) ->
@@ -825,7 +829,7 @@ and pr_atom1 = function
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) -> 
-      hov 1 (str (if ev then "erewrite" else "rewrite") ++ 
+      hov 1 (str (with_evars ev "rewrite") ++ 
 	     prlist_with_sep
 	     (fun () -> str ","++spc())
 	     (fun (b,m,c) -> 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d961dc2f2..e698a187c 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -372,18 +372,18 @@ let rec mlexpr_of_atomic_tactic = function
               $mlexpr_of_hyp id2$ >>
 
   (* Constructors *)
-  | Tacexpr.TacLeft l ->
-      <:expr< Tacexpr.TacLeft $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacRight l ->
-      <:expr< Tacexpr.TacRight $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacSplit (b,l) ->
+  | Tacexpr.TacLeft (ev,l) ->
+      <:expr< Tacexpr.TacLeft $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
+  | Tacexpr.TacRight (ev,l) ->
+      <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
+  | Tacexpr.TacSplit (ev,b,l) ->
       <:expr< Tacexpr.TacSplit
-        ($mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>>
-  | Tacexpr.TacAnyConstructor t ->
-      <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_option mlexpr_of_tactic t$>>
-  | Tacexpr.TacConstructor (n,l) ->
+        ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>>
+  | Tacexpr.TacAnyConstructor (ev,t) ->
+      <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>>
+  | Tacexpr.TacConstructor (ev,n,l) ->
       let n = mlexpr_of_or_metaid mlexpr_of_int n in
-      <:expr< Tacexpr.TacConstructor $n$ $mlexpr_of_binding_kind l$>>
+      <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $mlexpr_of_binding_kind l$>>
 
   (* Conversion *)
   | Tacexpr.TacReduce (r,cl) ->
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 242368ce9..e5632515d 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -261,8 +261,8 @@ let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
  * pose a value for it by constructing a fresh evar.  We do this in
  * left-to-right order, so that every evar's type is always closed w.r.t.
  * metas. *)
-let clenv_pose_dependent_evars clenv =
-  let dep_mvs = clenv_dependent false clenv in
+
+let clenv_pose_metas_as_evars clenv dep_mvs =
   List.fold_left
     (fun clenv mv ->
       let ty = clenv_meta_type clenv mv in
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 4f27ec902..dfa751349 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -79,7 +79,9 @@ val clenv_unique_resolver :
 val evar_clenv_unique_resolver :
   bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
 
-val clenv_pose_dependent_evars : clausenv -> clausenv
+val clenv_dependent : bool -> clausenv -> metavariable list
+
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 
 (***************************************************************)
 (* Bindings *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2703e5ae0..91b70e3b0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -674,5 +674,5 @@ let pr_evar_defs evd =
       str"METAS:"++brk(0,1)++pr_meta_map evd.metas in
   v 0 (pp_evm ++ cstrs ++ pp_met)
 
-let pr_metaset metas =
-  Metaset.fold (fun mv pp -> pr_meta mv ++ pp) metas (Pp.mt())
+let pr_metaset metas = 
+  str "[" ++ prlist_with_sep spc pr_meta (Metaset.elements metas) ++ str "]"
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 90a3728eb..05af1652e 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -92,7 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with
 let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
-    | Meta n -> PMeta (Some (id_of_string (string_of_int n)))
+    | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
     | Sort (Prop c) -> PSort (RProp c)
     | Sort (Type _) -> PSort (RType None)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 32df490db..ece3586a1 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -23,7 +23,7 @@ open Evd
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
-    with Not_found -> error ("unknown meta ?"^string_of_int mv) in
+    with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in
   meta_instance evd ty
 
 let constant_type_knowing_parameters env cst jl =
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index d133beaa9..60abc5d66 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -60,8 +60,16 @@ let clenv_cast_meta clenv =
   in 
   crec
 
+let clenv_pose_dependent_evars with_evars clenv =
+  let dep_mvs = clenv_dependent false clenv in
+  if dep_mvs <> [] & not with_evars then
+    raise
+      (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
+  clenv_pose_metas_as_evars clenv dep_mvs
+
+
 let clenv_refine with_evars clenv gls =
-  let clenv = if with_evars then clenv_pose_dependent_evars clenv else clenv in
+  let clenv = clenv_pose_dependent_evars with_evars clenv in
   tclTHEN
     (tclEVARS (evars_of clenv.evd)) 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 90d010c80..0cf0a5545 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -26,5 +26,7 @@ val clenv_refine : evars_flag -> clausenv -> tactic
 val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
+val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+
 (* Compatibility, use res_pf ?with_evars:true instead *)
 val e_res_pf : clausenv -> tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c9ae78103..24de605ac 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -32,8 +32,7 @@ type refiner_error =
 
   (* Errors raised by the refiner *)
   | BadType of constr * constr * constr
-  | OccurMeta of constr
-  | OccurMetaGoal of constr
+  | UnresolvedBindings of name list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
@@ -266,8 +265,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	if occur_meta conclty then
-          raise (RefinerError (OccurMetaGoal conclty));
+	if !check && occur_meta conclty then
+	  anomaly "refined called with a dependent meta";
 	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
     | Cast (t,_, ty) ->
@@ -302,7 +301,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	(acc'',conclty')
 
     | _ -> 
-	if occur_meta trm then raise (RefinerError (OccurMeta trm));
+	if occur_meta trm then
+	  anomaly "refiner called with a meta in non app/case subterm";
       	let t'ty = goal_type_of env sigma trm in
 	check_conv_leq_goal env sigma trm t'ty conclty;
         (goalacc,t'ty)
@@ -342,7 +342,10 @@ and mk_hdgoals sigma goal goalacc trm =
 	in
 	(acc'',conclty')
 
-    | _ -> goalacc, goal_type_of env sigma trm
+    | _ ->
+	if !check && occur_meta trm then
+	  anomaly "refined called with a dependent meta";
+	goalacc, goal_type_of env sigma trm
 
 and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 081d02f37..88e77fd7b 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -50,8 +50,7 @@ type refiner_error =
 
   (*i Errors raised by the refiner i*)
   | BadType of constr * constr * constr
-  | OccurMeta of constr
-  | OccurMetaGoal of constr
+  | UnresolvedBindings of name list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 595c2ec9b..7a90040e5 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -24,6 +24,7 @@ type lazy_flag = bool      (* true = lazy             false = eager *)
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
+type split_flag = bool     (* true = exists           false = split *)
 
 type raw_red_flag =
   | FBeta
@@ -179,11 +180,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacRevert of 'id list
 
   (* Constructors *)
-  | TacLeft of 'constr bindings
-  | TacRight of 'constr bindings
-  | TacSplit of bool * 'constr bindings
-  | TacAnyConstructor of 'tac option
-  | TacConstructor of int or_metaid * 'constr bindings
+  | TacLeft of evars_flag * 'constr bindings
+  | TacRight of evars_flag * 'constr bindings
+  | TacSplit of evars_flag * split_flag * 'constr bindings
+  | TacAnyConstructor of evars_flag * 'tac option
+  | TacConstructor of evars_flag * int or_metaid * 'constr bindings
 
   (* Conversion *)
   | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 9b0bb188b..5388bf207 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1138,7 +1138,7 @@ let declare_instance_trans binders a aeq n lemma =
   in anew_instance binders instance 
        [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
-let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) 
+let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
 
 let declare_relation ?(binders=[]) a aeq n refl symm trans = 
   init_setoid ();
@@ -1421,7 +1421,8 @@ let check_evar_map_of_evars_defs evd =
   Evd.Metaset.iter
    (fun m ->
      if Evd.meta_defined evd m then () else
-      raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
+      raise
+	(Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
  in
   List.iter
    (fun (_,binding) ->
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 74d6f9ccc..5c59e8244 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -55,69 +55,6 @@ let registered_e_assumption gl =
   tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
               (pf_ids_of_hyps gl)) gl
 
-let e_constructor_tac boundopt i lbind gl = 
-    let cl = pf_concl gl in 
-  let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
-  let nconstr =
-    Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  if i=0 then error "The constructors are numbered starting from 1";
-  if i > nconstr then error "Not enough constructors";
-  begin match boundopt with 
-    | Some expctdnum -> 
-        if expctdnum <> nconstr then 
-	  error "Not the expected number of constructors"
-    | None -> ()
-  end;
-  let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = eapply_with_ebindings (cons,lbind) in
-  (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast
-; intros; apply_tac]) gl
-
-let e_one_constructor i = e_constructor_tac None i
-
-let e_any_constructor tacopt gl =
-  let t = match tacopt with None -> tclIDTAC | Some t -> t in
-  let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
-  let nconstr =
-    Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  if nconstr = 0 then error "The type has no constructors";
-  tclFIRST (List.map (fun i -> tclTHEN (e_one_constructor i NoBindings) t) 
-              (interval 1 nconstr)) gl
-
-let e_left = e_constructor_tac (Some 2) 1
-
-let e_right = e_constructor_tac (Some 2) 2
-
-let e_split = e_constructor_tac (Some 1) 1
-
-(* This automatically define h_econstructor (among other things) *)
-TACTIC EXTEND econstructor
-  [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
-| [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
-| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (Option.map Tacinterp.eval_tactic t) ] 
-      END
-
-TACTIC EXTEND eleft
-  [ "eleft" "with" bindings(l) ] -> [e_left l]
-| [ "eleft"] -> [e_left NoBindings]
-END
-
-TACTIC EXTEND eright
-  [ "eright" "with" bindings(l) ] -> [e_right l]
-| [ "eright" ] -> [e_right NoBindings]
-END
-
-TACTIC EXTEND esplit
-  [ "esplit" "with" bindings(l) ] -> [e_split l]
-| [ "esplit"] -> [e_split NoBindings]
-END
-
-
-TACTIC EXTEND eexists
-  [ "eexists" bindings(l) ] -> [e_split l]
-END
-
-
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 18263127b..0cb314201 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -97,18 +97,18 @@ let h_rename l =
 let h_revert l = abstract_tactic (TacRevert l) (revert l)
 
 (* Constructors *)
-let h_left l    = abstract_tactic (TacLeft l) (left_with_ebindings l)
-let h_right l   = abstract_tactic (TacLeft l) (right_with_ebindings l)
-let h_split l   = abstract_tactic (TacSplit (false,l)) (split_with_ebindings l)
-(* Moved to tacinterp because of dependence in Tacinterp.interp
+let h_left ev l  = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
+let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l)
+let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
+(* Moved to tacinterp because of dependencies in Tacinterp.interp
 let h_any_constructor t =
   abstract_tactic (TacAnyConstructor t) (any_constructor t)
 *)
-let h_constructor n l =
-  abstract_tactic (TacConstructor(AI n,l))(constructor_tac None n l)
-let h_one_constructor n = h_constructor n NoBindings
-let h_simplest_left   = h_left NoBindings
-let h_simplest_right  = h_right NoBindings
+let h_constructor ev n l =
+  abstract_tactic (TacConstructor(ev,AI n,l))(constructor_tac ev None n l)
+let h_one_constructor n = h_constructor false n NoBindings
+let h_simplest_left   = h_left false NoBindings
+let h_simplest_right  = h_right false NoBindings
 
 (* Conversion *)
 let h_reduce r cl  = 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 84a571937..8cbc28d1e 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -80,10 +80,10 @@ val h_rename          : (identifier*identifier) list -> tactic
 val h_revert          : identifier list -> tactic
 
 (* Constructors *)
-val h_constructor     : int -> open_constr bindings -> tactic
-val h_left            : open_constr bindings -> tactic
-val h_right           : open_constr bindings -> tactic
-val h_split           : open_constr bindings -> tactic
+val h_constructor     : evars_flag -> int -> open_constr bindings -> tactic
+val h_left            : evars_flag -> open_constr bindings -> tactic
+val h_right           : evars_flag -> open_constr bindings -> tactic
+val h_split           : evars_flag -> open_constr bindings -> tactic
 
 val h_one_constructor : int -> tactic
 val h_simplest_left   : tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 55b8d08c6..03eaf2d4d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -449,16 +449,15 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
 let raw_inversion inv_kind id status names gl =
   let env = pf_env gl and sigma = project gl in
   let c = mkVar id in
-  let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
+  let (ind,t) = 
+    try pf_reduce_to_quantified_ind gl (pf_type_of gl c)
+    with UserError _ -> 
+      errorlabstrm "raw_inversion"
+	(str ("The type of "^(string_of_id id)^" is not inductive")) in
   let indclause = mk_clenv_from gl (c,t) in
-  let newc = clenv_value indclause in
   let ccl = clenv_type indclause in
   check_no_metas indclause ccl;
-  let IndType (indf,realargs) =
-    try find_rectype env sigma ccl
-    with Not_found ->
-      errorlabstrm "raw_inversion"
-	(str ("The type of "^(string_of_id id)^" is not inductive")) in
+  let IndType (indf,realargs) = find_rectype env sigma ccl in
   let (elim_predicate,neqns) =
     make_inv_predicate env sigma indf realargs id status (pf_concl gl) in
   let (cut_concl,case_tac) =
@@ -473,7 +472,7 @@ let raw_inversion inv_kind id status names gl =
      (true_cut Anonymous cut_concl)
      [case_tac names 
        (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
-       (Some elim_predicate) ([],[]) newc;
+       (Some elim_predicate) ([],[]) ind indclause;
       onLastHyp
         (fun id ->
            (tclTHEN
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 9f8821341..69840f85c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1712,7 +1712,7 @@ let check_evar_map_of_evars_defs evd =
   Evd.Metaset.iter
    (fun m ->
      if Evd.meta_defined evd m then () else
-      raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
+      raise (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
  in
   List.iter
    (fun (_,binding) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9a2c2097c..aba96afb3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -215,10 +215,14 @@ let _ =
         "cofix", TacCofix None;
         "trivial", TacTrivial ([],None);
         "auto", TacAuto(None,[],None);
-        "left", TacLeft NoBindings;
-        "right", TacRight NoBindings;
-        "split", TacSplit(false,NoBindings);
-        "constructor", TacAnyConstructor None;
+        "left", TacLeft(false,NoBindings);
+        "eleft", TacLeft(true,NoBindings);
+        "right", TacRight(false,NoBindings);
+        "eright", TacRight(true,NoBindings);
+        "split", TacSplit(false,false,NoBindings);
+        "esplit", TacSplit(true,false,NoBindings);
+        "constructor", TacAnyConstructor (false,None);
+        "econstructor", TacAnyConstructor (true,None);
         "reflexivity", TacReflexivity;
         "symmetry", TacSymmetry nocl
       ];
@@ -721,11 +725,11 @@ let rec intern_atomic lf ist x =
   | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
 	
   (* Constructors *)
-  | TacLeft bl -> TacLeft (intern_bindings ist bl)
-  | TacRight bl -> TacRight (intern_bindings ist bl)
-  | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
-  | TacAnyConstructor t -> TacAnyConstructor (Option.map (intern_tactic ist) t)
-  | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)
+  | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
+  | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
+  | TacSplit (ev,b,bl) -> TacSplit (ev,b,intern_bindings ist bl)
+  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t)
+  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
@@ -2083,14 +2087,14 @@ and interp_atomic ist gl = function
   | TacRevert l -> h_revert (interp_hyp_list ist gl l)
 
   (* Constructors *)
-  | TacLeft bl -> h_left (interp_bindings ist gl bl)
-  | TacRight bl -> h_right (interp_bindings ist gl bl)
-  | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
-  | TacAnyConstructor t ->
-      abstract_tactic (TacAnyConstructor t)
-        (Tactics.any_constructor (Option.map (interp_tactic ist) t))
-  | TacConstructor (n,bl) ->
-      h_constructor (skip_metaid n) (interp_bindings ist gl bl)
+  | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl)
+  | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl)
+  | TacSplit (ev,_,bl) -> h_split ev (interp_bindings ist gl bl)
+  | TacAnyConstructor (ev,t) ->
+      abstract_tactic (TacAnyConstructor (ev,t))
+        (Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
+  | TacConstructor (ev,n,bl) ->
+      h_constructor ev (skip_metaid n) (interp_bindings ist gl bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
@@ -2391,11 +2395,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacRevert _ as x -> x
 
   (* Constructors *)
-  | TacLeft bl -> TacLeft (subst_bindings subst bl)
-  | TacRight bl -> TacRight (subst_bindings subst bl)
-  | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
-  | TacAnyConstructor t -> TacAnyConstructor (Option.map (subst_tactic subst) t)
-  | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)
+  | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
+  | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
+  | TacSplit (ev,b,bl) -> TacSplit (ev,b,subst_bindings subst bl)
+  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
+  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9bb6eef2c..dd8aa1294 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,11 +324,11 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) -> array_last cl
   | _ -> anomaly "last_arg"
 
-let general_elim_then_using 
-  elim isrec allnames tac predicate (indbindings,elimbindings) c gl =
-  let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+let general_elim_then_using mk_elim 
+  isrec allnames tac predicate (indbindings,elimbindings) 
+  ind indclause gl =
+  let elim = mk_elim ind gl in
   (* applying elimination_scheme just a little modified *)
-  let indclause  = mk_clenv_from gl (c,t) in
   let indclause' = clenv_match_args indbindings indclause in
   let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
   let indmv = 
@@ -351,7 +351,7 @@ let general_elim_then_using
   in
   let elimclause' = clenv_fchain indmv elimclause indclause' in
   let elimclause' = clenv_match_args elimbindings elimclause' in
-  let branchsigns = compute_construtor_signatures isrec ity in
+  let branchsigns = compute_construtor_signatures isrec ind in
   let brnames = compute_induction_names (Array.length branchsigns) allnames in
   let after_tac ce i gl =
     let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in
@@ -362,7 +362,7 @@ let general_elim_then_using
                    (fun acc b -> if b then acc+2 else acc+1)
                    0 branchsigns.(i);
                branchnum = i+1;
-               ity = ity;
+               ity = ind;
                largs = List.map (clenv_nf_meta ce) largs;
                pred = clenv_nf_meta ce hd }
     in 
@@ -377,37 +377,32 @@ let general_elim_then_using
   in 
   elim_res_pf_THEN_i elimclause' branchtacs gl
 
+(* computing the case/elim combinators *)
+
+let gl_make_elim ind gl =
+  Indrec.lookup_eliminator ind (elimination_sort_of_goal gl)
+
+let gl_make_case_dep ind gl =
+  pf_apply Indrec.make_case_dep gl ind (elimination_sort_of_goal gl)
+
+let gl_make_case_nodep ind gl =
+  pf_apply Indrec.make_case_nodep gl ind (elimination_sort_of_goal gl)
 
-let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
+let elimination_then_using tac predicate bindings c gl = 
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let elim =
-    Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
-  general_elim_then_using
-    elim true IntroAnonymous tac predicate (indbindings,elimbindings) c gl
+  let indclause  = mk_clenv_from gl (c,t) in
+  general_elim_then_using gl_make_elim
+    true IntroAnonymous tac predicate bindings ind indclause gl
+
+let case_then_using =
+  general_elim_then_using gl_make_case_dep false
 
+let case_nodep_then_using =
+  general_elim_then_using gl_make_case_nodep false
 
 let elimination_then tac        = elimination_then_using tac None 
 let simple_elimination_then tac = elimination_then tac ([],[])
 
-let case_then_using allnames tac predicate (indbindings,elimbindings) c gl =
-  (* finding the case combinator *)
-  let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sigma = project gl in 
-  let sort  = elimination_sort_of_goal gl  in
-  let elim  = Indrec.make_case_dep (pf_env gl) sigma ity sort in  
-  general_elim_then_using 
-    elim false allnames tac predicate (indbindings,elimbindings) c gl
-
-let case_nodep_then_using allnames tac predicate (indbindings,elimbindings)
-  c gl =
-  (* finding the case combinator *)
-  let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sigma = project gl in 
-  let sort  = elimination_sort_of_goal gl  in
-  let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
-  general_elim_then_using 
-    elim false allnames tac predicate (indbindings,elimbindings) c gl
-
 
 let make_elim_branch_assumptions ba gl =   
   let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index dd3b73135..d7620acf2 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -138,9 +138,9 @@ val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
 
 val general_elim_then_using :
-  constr -> (* isrec: *) bool -> intro_pattern_expr ->
+  (inductive -> goal sigma -> constr) -> rec_flag -> intro_pattern_expr ->
     (branch_args -> tactic) -> constr option -> 
-      (arg_bindings * arg_bindings) -> constr -> tactic
+      (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic
 	  
 val elimination_then_using :
   (branch_args -> tactic) -> constr option -> 
@@ -152,11 +152,13 @@ val elimination_then :
 
 val case_then_using :
   intro_pattern_expr -> (branch_args -> tactic) -> 
-    constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
+    constr option -> (arg_bindings * arg_bindings) ->
+      inductive -> clausenv -> tactic
 
 val case_nodep_then_using :
   intro_pattern_expr -> (branch_args -> tactic) -> 
-    constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
+    constr option -> (arg_bindings * arg_bindings) -> 
+      inductive -> clausenv -> tactic
 
 val simple_elimination_then :
   (branch_args -> tactic) -> constr -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 963025c3b..b4e646a07 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -528,7 +528,7 @@ let error_uninstantiated_metas t clenv =
   in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
 
 let clenv_refine_in with_evars id clenv gl =
-  let clenv = if with_evars then clenv_pose_dependent_evars clenv else clenv in
+  let clenv = clenv_pose_dependent_evars with_evars clenv in
   let new_hyp_typ  = clenv_type clenv in
   if not with_evars & occur_meta new_hyp_typ then 
     error_uninstantiated_metas new_hyp_typ clenv;
@@ -672,9 +672,9 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (* Resolution with missing arguments *)
 
-let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
+let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   let flags = 
-    if advanced then default_unify_flags else default_no_delta_unify_flags in
+    if with_delta then default_unify_flags else default_no_delta_unify_flags in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
@@ -700,7 +700,8 @@ let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
 	   second order unification *)
 	try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
 	with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
-	  if advanced then
+	  if with_destruct then
+	   try
 	    let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
 	    match match_with_conjunction (snd (decompose_prod t)) with
 	    | Some _ ->
@@ -717,14 +718,15 @@ let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
 			tclTHEN (try_main_apply (mkVar id)) (thin l)) l))
 		]) gl
 	    | None ->
-	      raise exn
+		raise Exit
+	   with RefinerError _|UserError _|Exit -> raise exn 
 	  else
-	    raise exn in
+	    raise exn
+ in
     try_red_apply thm_ty0 in
   try_main_apply c gl
 
-let advanced_apply_with_ebindings = apply_with_ebindings_gen true false
-let advanced_eapply_with_ebindings = apply_with_ebindings_gen true true
+let apply_with_ebindings_gen b = general_apply b b
 
 let apply_with_ebindings = apply_with_ebindings_gen false false
 let eapply_with_ebindings = apply_with_ebindings_gen false true
@@ -942,45 +944,47 @@ let check_number_of_constructors expctdnumopt i nconstr =
   end;
   if i > nconstr then error "Not enough constructors"
 
-let constructor_tac expctdnumopt i lbind gl =
+let constructor_tac with_evars expctdnumopt i lbind gl =
   let cl = pf_concl gl in 
   let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
   check_number_of_constructors expctdnumopt i nconstr;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = advanced_apply_with_ebindings (cons,lbind) in
+  let apply_tac = general_apply true false with_evars (cons,lbind) in
   (tclTHENLIST 
      [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
 
-let one_constructor i = constructor_tac None i
+let one_constructor i = constructor_tac false None i
 
 (* Try to apply the constructor of the inductive definition followed by 
    a tactic t given as an argument.
    Should be generalize in Constructor (Fun c : I -> tactic)
  *)
 
-let any_constructor tacopt gl =
+let any_constructor with_evars tacopt gl =
   let t = match tacopt with None -> tclIDTAC | Some t -> t in
   let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
   if nconstr = 0 then error "The type has no constructors";
-  tclFIRST (List.map (fun i -> tclTHEN (one_constructor i NoBindings) t) 
-              (interval 1 nconstr)) gl
+  tclFIRST
+    (List.map
+      (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t) 
+      (interval 1 nconstr)) gl
 
-let left_with_ebindings  = constructor_tac (Some 2) 1
-let right_with_ebindings = constructor_tac (Some 2) 2
-let split_with_ebindings = constructor_tac (Some 1) 1
+let left_with_ebindings  with_evars = constructor_tac with_evars (Some 2) 1
+let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2
+let split_with_ebindings with_evars = constructor_tac with_evars (Some 1) 1
 
-let left l         = left_with_ebindings (inj_ebindings l)
-let simplest_left  = left NoBindings
+let left l             = left_with_ebindings false (inj_ebindings l)
+let simplest_left      = left NoBindings
 
-let right l        = right_with_ebindings (inj_ebindings l)
-let simplest_right = right NoBindings
+let right l            = right_with_ebindings false (inj_ebindings l)
+let simplest_right     = right NoBindings
 
-let split l        = split_with_ebindings (inj_ebindings l)
-let simplest_split = split NoBindings
+let split l            = split_with_ebindings false (inj_ebindings l)
+let simplest_split     = split NoBindings
 
 
 (*****************************)
@@ -1742,13 +1746,14 @@ let make_base n id =
 let make_up_names n ind_opt cname = 
   let is_hyp = atompart_of_id cname = "H" in
   let base = string_of_id (make_base n cname) in
+  let ind_prefix = "IH" in
   let base_ind = 
     if is_hyp then 
       match ind_opt with
-	| None -> id_of_string ""
-	| Some ind_id -> Nametab.id_of_global ind_id 
-    else cname in
-  let hyprecname = add_prefix "IH" (make_base n base_ind) in
+	| None -> id_of_string ind_prefix
+	| Some ind_id -> add_prefix ind_prefix (Nametab.id_of_global ind_id)
+    else add_prefix ind_prefix cname in
+  let hyprecname = make_base n base_ind in
   let avoid =
     if n=1 (* Only one recursive argument *) or n=0 then []
     else
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1c64e47e8..1b2b7b38f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -182,9 +182,6 @@ val eapply_with_bindings  : constr with_bindings -> tactic
 val apply_with_ebindings  : constr with_ebindings -> tactic
 val eapply_with_ebindings : constr with_ebindings -> tactic
 
-val advanced_apply_with_ebindings  : constr with_ebindings -> tactic
-val advanced_eapply_with_ebindings : constr with_ebindings -> tactic
-
 val cut_and_apply         : constr -> tactic
 
 val apply_in : evars_flag -> identifier -> constr with_ebindings list -> tactic
@@ -282,22 +279,22 @@ val dorE : bool -> clause ->tactic
 
 (*s Introduction tactics. *)
 
-val constructor_tac            : int option -> int -> 
-                                 open_constr bindings  -> tactic
-val one_constructor            : int -> open_constr bindings  -> tactic
-val any_constructor            : tactic option -> tactic
+val constructor_tac      : evars_flag -> int option -> int -> 
+                           open_constr bindings  -> tactic
+val any_constructor      : evars_flag -> tactic option -> tactic
+val one_constructor      : int -> open_constr bindings  -> tactic
 
-val left                       : constr bindings -> tactic
-val right                      : constr bindings -> tactic
-val split                      : constr bindings -> tactic
+val left                 : constr bindings -> tactic
+val right                : constr bindings -> tactic
+val split                : constr bindings -> tactic
 
-val left_with_ebindings        : open_constr bindings -> tactic
-val right_with_ebindings       : open_constr bindings -> tactic
-val split_with_ebindings       : open_constr bindings -> tactic
+val left_with_ebindings  : evars_flag -> open_constr bindings -> tactic
+val right_with_ebindings : evars_flag -> open_constr bindings -> tactic
+val split_with_ebindings : evars_flag -> open_constr bindings -> tactic
 
-val simplest_left              : tactic
-val simplest_right             : tactic
-val simplest_split             : tactic
+val simplest_left        : tactic
+val simplest_right       : tactic
+val simplest_split       : tactic
 
 (*s Logical connective tactics. *)
 
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index ada292f18..02f88b727 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -29,3 +29,10 @@ Goal forall n, n = S n.
 induction S.
 Abort.
 
+(* Check that elimination with remaining evars do not raise an bad
+   error message *)
+
+Theorem Refl : forall P, P <-> P. tauto. Qed.
+Goal True.
+case Refl || ecase Refl.
+Abort.
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 10d64dcf8..325debad3 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -55,7 +55,8 @@ let add_ml_include s =
   Mltop.add_ml_dir s
 
 (* Puts dir in the path of ML and in the LoadPath *)
-let coq_add_path s = Mltop.add_path s (Names.make_dirpath [Nameops.coq_root])
+let coq_add_path d s =
+  Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
 let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nameops.coq_root])
 
 (* By the option -include -I or -R of the command line *)
@@ -95,21 +96,21 @@ let theories_dirs_map = [
 
 (* Initializes the LoadPath according to COQLIB and Coq_config *)
 let init_load_path () =
-  (* developper specific directories to open *)
-  let dev = if Coq_config.local then [ "dev" ] else [] in
   let coqlib =
     (* variable COQLIB overrides the default library *)
     getenv_else "COQLIB"
       (if Coq_config.local || !Flags.boot then Coq_config.coqtop
 	else Coq_config.coqlib) in
   let user_contrib = coqlib/"user-contrib" in
-  let dirs = "states" :: "contrib" :: dev in
+  let dirs = "states" :: ["contrib"] in
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
     (* first user-contrib *)
     if Sys.file_exists user_contrib then 
       Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
     (* then states, contrib and dev *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
+    (* developer specific directory to open *)
+    if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* then standard library *)
     List.iter 
       (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b9f187784..505f456db 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -508,22 +508,19 @@ let explain_typeclass_error env err =
 (* Refiner errors *)
 
 let explain_refiner_bad_type arg ty conclty =
-  str "refiner was given an argument" ++ brk(1,1) ++
+  str "Refiner was given an argument" ++ brk(1,1) ++
   pr_lconstr arg ++ spc () ++
   str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
   str "instead of" ++ brk(1,1) ++ pr_lconstr conclty
 
-let explain_refiner_occur_meta t =
-  str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++
-  spc () ++ str "because there are metavariables, and it is" ++
-  spc () ++ str "neither an application nor a Case"
-
-let explain_refiner_occur_meta_goal t =
-  str "generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++
-  spc () ++ str "has metavariables in it"
+let explain_refiner_unresolved_bindings l =
+  let l = map_succeed (function Name id -> id | _ -> failwith "") l in
+  str "Unable to find an instance for the " ++ 
+  str (plural (List.length l) "variable") ++ spc () ++
+  prlist_with_sep pr_coma pr_id l
 
 let explain_refiner_cannot_apply t harg =
-  str "in refiner, a term of type " ++ brk(1,1) ++
+  str "In refiner, a term of type " ++ brk(1,1) ++
   pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
   pr_lconstr harg
 
@@ -538,13 +535,12 @@ let explain_does_not_occur_in c hyp =
   str "does not occur in" ++ spc () ++ pr_id hyp ++ str "."
 
 let explain_non_linear_proof c =
-  str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
+  str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
   spc () ++ str "because a metavariable has several occurrences."
 
 let explain_refiner_error = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
-  | OccurMeta t -> explain_refiner_occur_meta t
-  | OccurMetaGoal t -> explain_refiner_occur_meta_goal t
+  | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
   | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
   | NotWellTyped c -> explain_refiner_not_well_typed c
   | IntroNeedsProduct -> explain_intro_needs_product ()
@@ -611,7 +607,7 @@ let error_bad_entry () =
   str "Bad inductive definition."
 
 let error_not_allowed_case_analysis dep kind i =
-  str (if dep then "Dependent" else "Non Dependent") ++
+  str (if dep then "Dependent" else "Non dependent") ++
   str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++
   str "is not allowed for inductive definition: " ++
   pr_inductive (Global.env()) i ++ str "."