29 files changed, 310 insertions, 159 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index da5b425794..241ec35861 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -68,7 +68,7 @@
 : ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}
 
 ########################################################################
-# Coquelicot
+# CompCert
 ########################################################################
 : ${CompCert_CI_BRANCH:=master}
 : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
diff --git a/dev/doc/api.txt b/dev/doc/api.txt
new file mode 100644
index 0000000000..5827257b53
--- /dev/null
+++ b/dev/doc/api.txt
@@ -0,0 +1,10 @@
+Recommendations in using the API:
+
+The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
+
+- On type constr, the canonical equality on CIC (up to
+  alpha-conversion and cast removal) is Constr.equal
+- The type constr is abstract, use mkRel, mkSort, etc. to build
+  elements in constr; use "kind_of_term" to analyze the head of a
+  constr; use destRel, destSort, etc. when the head constructor is
+  known
diff --git a/dev/doc/style.txt b/dev/doc/style.txt
index 27695a09b1..2ee3dadd77 100644
--- a/dev/doc/style.txt
+++ b/dev/doc/style.txt
@@ -1,75 +1,142 @@
-
-<< L'uniformité du style est plus importante que le style lui-même. >>
-(Kernigan & Pike, The Practice of Programming)
-
-Mode Emacs
-==========
-   Tuareg, que l'on trouve ici :  http://www.prism.uvsq.fr/~acohen/tuareg/
-
-   avec le réglage suivant :     (setq tuareg-in-indent 2)
-
-Types récursifs et filtrages
-============================
-   Une barre de séparation y compris sur le premier constructeur
-
-type t =
-  | A 
-  | B of machin
-
-match expr with
-  | A -> ...
-  | B x -> ...
-
-Remarque : à partir de la 8.2 environ, la tendance est à utiliser le
-format suivant qui permet de limiter l'escalade d'indentation tout en
-produisant un aspect visuel intéressant de bloc :
-
-type t =
-| A 
-| B of machin
-
-match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = function
-| A -> ...
-| B x -> ...
-
-Le deuxième cas est obtenu sous tuareg avec les réglages
-
-  (setq tuareg-with-indent 0)
-  (setq tuareg-function-indent 0)
-  (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien 
-                                      /// pour les let mais pas pour les let-in
-
-Conditionnelles
-===============
-  if condition then
-    premier-cas
-  else
-    deuxieme-cas
-
-  Si effets de bord dans les branches, utilisez begin ... end et non des
-  parenthèses i.e.
-
-  if condition then begin
-    instr1;
-    instr2
-  end else begin
-    instr3;
-    instr4
-  end
-    
-  Si la première branche lève une exception, évitez le else i.e.
-
-    if condition then                     if condition then error "machin";
-      error "machin"          ----->      suite
+<< Style uniformity is more important than style itself >>
+   (Kernigan & Pike, The Practice of Programming)
+
+OCaml Style:
+- Spacing and indentation
+  - indent your code (using tuareg default)
+  - no strong constraints in formatting "let in"; possible styles are:
+    "let x = ... in"
+    "let x =
+       ... in"
+    "let
+       x = ...
+     in"
+  - but: no extra indentation before a "in" coming on next line,
+    otherwise, it first shifts further and further on the right,
+    reducing the amount of space available; second, it is not robust to
+    insertion of a new "let"
+  - it is established usage to have space around "|" as in
+    "match c with
+     | [] | [a] -> ...
+     | a::b::l -> ..."
+  - in a one-line "match", it is preferred to have no "|" in front of
+    the first case (this saves spaces for the match to hold in the line)
+  - from about 8.2, the tendency is to use the following format which
+    limit excessive indentation while providing an interesting "block" aspect
+    type t =
+    | A 
+    | B of machin
+
+    let f expr = match expr with
+    | A -> ...
+    | B x -> ...
+
+    let f expr = function
+    | A -> ...
+    | B x -> ...
+  - add spaces around = and == (make the code "breaths")
+  - the common usage is to write "let x,y = ... in ..." rather than
+    "let (x,y) = ... in ..."
+  - parenthesizing with either "(" and ")" or with "begin" and "end" is
+    common practice
+  - preferred layout for conditionals:
+    if condition then
+      premier-cas
     else
-      suite
-
-  
+      deuxieme-cas
+  - in case of effects in branches, use "begin ... end" rather than
+    parentheses
+    if condition then begin
+      instr1;
+      instr2
+    end else begin
+      instr3;
+      instr4
+    end
+  - if the first branch raises an exception, avoid the "else", i.e.:
+    if condition then                     if condition then error "foo";
+      error "foo"          ----->         bar
+    else
+      bar
+  - it is the usage not to use ;; to end OCaml sentences (however,
+    inserting ";;" can be useful for debugging syntax errors crossing
+    the boundary of functions)
+  - relevant options in tuareg:
+    (setq tuareg-in-indent 2)
+    (setq tuareg-with-indent 0)
+    (setq tuareg-function-indent 0)
+    (setq tuareg-let-always-indent nil)
+
+- Coding methodology
+  - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C),
+    Out_of_memory, Stack_overflow, etc.
+    at least, use "try with e when Errors.noncritical e -> ..."
+    (to be detailed, Pierre L. ?)
+  - do not abuse of fancy combinators: sometimes what a "let rec" loop
+    does is more readable and simpler to grasp than what a "fold" does
+  - do not break abstractions: if an internal property is hidden
+    behind an interface, do no rely on it in code which uses this
+    interface (e.g. do not use List.map thinking it is left-to-right,
+    use map_left)
+  - in particular, do not use "=" on abstract types: there is no
+    reason a priori that it is the intended equality on this type; use the
+    "equal" function normally provided with the abstract type
+  - avoid polymorphically typed "=" whose implementation is not
+    optimized in OCaml and which has moreover no reason to be the
+    intended implementation of the equality when it comes to be
+    instantiated on a particular type (e.g. use List.mem_f,
+    List.assoc_f, rather than List.mem, List.assoc, etc, unless it is
+    absolutely clear that "=" will implement the intended equality, and
+    with the right complexity)
+  - any new general-purpose enough combinator on list should be put in
+    cList.ml, on type option in cOpt.ml, etc.
+  - unless of a good reason not to so, follow the style of the
+    surrounding code in the same file as much as possible,
+    the general guidelines are otherwise "let spacing breaths" (we
+    have large screen nowadays), "make your code easy to read and
+    to understand"
+  - document what is tricky, but do not overdocument, sometimes the
+    choice of names and the structuration of the code is a better
+    documentation than a long discourse; use of unicode in comments is
+    welcome if it can make comments more readable (then
+    "toggle-enable-multibyte-characters" can help when using the
+    debugger in emacs)
+  - all of initial "open File", or of small-scope File.(...), or
+    per-ident File.foo are common practices
+
+- Choice of variable names
+  - be consistent when naming from one function to another
+  - be consistent with the naming adopted in the functions from the
+    same file, or with the naming used elsewhere by similar functions
+  - use variable names which express meaning
+  - keep "cst" for constants and avoid it for constructors which is
+    otherwise a source of confusion
+  - for constructors, use "cstr" in type constructor (resp. "cstru" in
+    constructor puniverse); avoid "constr" for "constructor" which
+    could be think as the name of an arbitrary Constr.t
+  - for inductive types, use "ind" in the type inductive (resp "indu"
+    in inductive puniverse)
+  - for env, use "env"
+  - for evar_map, use "sigma", with tolerance into "evm" and "evd"
+  - for named_context or rel_context, use "ctxt" or "ctx" (or "sign")
+  - for formal/actual indices of inductive types: "realdecls", "realargs"
+  - for formal/actual parameters of inductive types: "paramdecls", "paramargs"
+  - for terms, use e.g. c, b, a, ...
+  - if a term is known to be a function: f, ...
+  - if a term is known to be a type: t, u, typ, ...
+  - for a declaration, use d or "decl"
+  - for errors, exceptions, use e
+
+- Common OCaml pitfalls
+  - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in
+    "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in
+    parentheses are needed around the "try" and the inner "match"
+  - even if stream are lazy, the Pp.(++) combinator is strict and
+    forces the evaluation of its arguments (use a "lazy" or a "fun () ->")
+    to make it lazy explicitly
+  - in "if ... then ... else ... ++ ...", the default parenthesizing
+    is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..."
+  - in "let myspecialfun = mygenericfun args", be sure that it does no
+    do side-effect; prefer otherwise "let mygenericfun arg =
+    mygenericfun args arg" to ensure that the function is evaluated at
+    runtime
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c37367de5b..16c822b6a5 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -477,15 +477,15 @@ names.
 \item{\tt Show Intro.}\comindex{Show Intro}\\
 If the current goal begins by at least one product, this command
 prints the name of the first product, as it would be generated by 
-an anonymous {\tt Intro}. The aim of this command is to ease the
+an anonymous {\tt intro}. The aim of this command is to ease the
 writing of more robust scripts. For example, with an appropriate 
 {\ProofGeneral} macro, it is possible to transform any anonymous {\tt
-  Intro} into a qualified one such as {\tt Intro y13}.
+  intro} into a qualified one such as {\tt intro y13}.
 In the case of a non-product goal, it prints nothing. 
 
 \item{\tt Show Intros.}\comindex{Show Intros}\\
 This command is similar to the previous one, it simulates the naming 
-process of an {\tt Intros}.
+process of an {\tt intros}.
 
 \item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
 \\ It displays
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 8605dda3a0..33ca2c629b 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -82,14 +82,14 @@ let make_var = function
   | ExtNonTerminal (_, p) -> Some p
   | _ -> assert false
 
-let declare_tactic loc s c cl = match cl with
+let declare_tactic loc tacname ~level classification clause = match clause with
 | [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
   (** The extension is only made of a name followed by constr entries: we do not
       add any grammar nor printing rule and add it as a true Ltac definition. *)
   let patt = make_patt rem in
   let vars = List.map make_var rem in
   let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
-  let entry = mlexpr_of_string s in
+  let entry = mlexpr_of_string tacname in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
   let name = mlexpr_of_string name in
@@ -117,13 +117,14 @@ let declare_tactic loc s c cl = match cl with
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
       TacML tactic. *)
-  let entry = mlexpr_of_string s in
+  let entry = mlexpr_of_string tacname in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let gl = mlexpr_of_clause cl in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
+  let gl = mlexpr_of_clause clause in
+  let level = mlexpr_of_int level in
+  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
-        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
+        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
         Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
     ]
 
@@ -134,20 +135,17 @@ EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
+        level = OPT [ "AT"; "LEVEL"; level = INT -> level ];
         c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
-         declare_tactic loc s c l ] ]
+        let level = match level with Some i -> int_of_string i | None -> 0 in
+         declare_tactic loc s ~level c l ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
         c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ];
-        "->"; "["; e = Pcaml.expr; "]" ->
-	(match l with
-	  | ExtNonTerminal _ :: _ ->
-	    (* En attendant la syntaxe de tacticielles *)
-	    failwith "Tactic syntax must start with an identifier"
-	  | _ -> (l,c,e))
+        "->"; "["; e = Pcaml.expr; "]" -> (l,c,e)
     ] ]
   ;
   tacargs:
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index e4f595ac4a..33dc2a335c 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -28,7 +28,7 @@ and 'constr intro_pattern_action_expr =
   | IntroWildcard
   | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
   | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
-  | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
+  | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr)
   | IntroRewrite of bool
 and 'constr or_and_intro_pattern_expr =
   | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 130f1eb039..f147ea3433 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -136,7 +136,7 @@ let dump (otab,_) =
   let disch_table = Array.make n a_discharge in
   let f2t_map = ref FMap.empty in
   Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 ~greedy:true cu in
+    let c, u = Future.split2 cu in
     Future.sink u;
     Future.sink c;
     opaque_table.(n) <- c;
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b9cf8101da..22b7eebcb4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -190,7 +190,7 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+        Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
           let body, uctx, signatures =
             inline_side_effects env body uctx side_eff in
           let valid_signatures = check_signatures trust signatures in
@@ -415,7 +415,7 @@ let export_side_effects mb env ce =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
-        const_entry_body = Future.chain ~greedy:true ~pure:true body
+        const_entry_body = Future.chain ~pure:true body
           (fun (b_ctx, _) -> b_ctx, []) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
@@ -497,7 +497,7 @@ let translate_local_def mb env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let inline_entry_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~greedy:true ~pure:true
+  const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
       (body, ctx'), []);
diff --git a/lib/future.ml b/lib/future.ml
index ea0382a63d..b60b32bb61 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -191,9 +191,9 @@ let transactify f x =
 let purify_future f x = if is_over x then f x else purify f x
 let compute x = purify_future (compute ~pure:false) x
 let force ~pure x = purify_future (force ~pure) x
-let chain ?(greedy=true) ~pure x f =
+let chain ~pure x f =
   let y = chain ~pure x f in
-  if is_over x && greedy then ignore(force ~pure y);
+  if is_over x then ignore(force ~pure y);
   y
 let force x = force ~pure:false x
 
@@ -204,13 +204,13 @@ let join kx =
 
 let sink kx = if is_val kx then ignore(join kx)
 
-let split2 ?greedy x =
-  chain ?greedy ~pure:true x (fun x -> fst x),
-  chain ?greedy ~pure:true x (fun x -> snd x)
+let split2 x =
+  chain ~pure:true x (fun x -> fst x),
+  chain ~pure:true x (fun x -> snd x)
 
-let map2 ?greedy f x l =
+let map2 f x l =
   CList.map_i (fun i y ->
-    let xi = chain ?greedy ~pure:true x (fun x ->
+    let xi = chain ~pure:true x (fun x ->
         try List.nth x i
         with Failure _ | Invalid_argument _ ->
           CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in
diff --git a/lib/future.mli b/lib/future.mli
index c780faf324..2a025ae844 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -113,8 +113,9 @@ val is_exn : 'a computation -> bool
 val peek_val : 'a computation -> 'a option
 val uuid : 'a computation -> UUID.t
 
-(* [chain greedy pure c f] chains computation [c] with [f].
- * The [greedy] and [pure] parameters are tricky:
+(* [chain pure c f] chains computation [c] with [f].
+ * [chain] forces immediately the new computation if the old one is_over (Exn or Val).
+ * The [pure] parameter is tricky:
  * [pure]:
  *   When pure is true, the returned computation will not keep a copy
  *   of the global state.
@@ -124,10 +125,8 @@ val uuid : 'a computation -> UUID.t
  *   one forces c' and then c''.
  *   [join c; chain ~pure:false c g] is invalid and fails at runtime.
  *   [force c; chain ~pure:false c g] is correct.
- * [greedy]:
- *   The [greedy] parameter forces immediately the new computation if
- *   the old one is_over (Exn or Val). Defaults to true. *)
-val chain : ?greedy:bool -> pure:bool ->
+ *)
+val chain : pure:bool ->
   'a computation -> ('a -> 'b) -> 'b computation
 
 (* Forcing a computation *)
@@ -143,9 +142,9 @@ val join : 'a computation -> 'a
 val sink : 'a computation -> unit
 
 (*** Utility functions ************************************************* ***)
-val split2 : ?greedy:bool ->
+val split2 :
   ('a * 'b) computation -> 'a computation * 'b computation
-val map2 : ?greedy:bool ->
+val map2 :
   ('a computation -> 'b -> 'c) ->
      'a list computation -> 'b list -> 'c list
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 685c07c9a8..fa01baab75 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -325,8 +325,9 @@ GEXTEND Gram
         l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
           let loc0,pat = pat in
           let f c pat =
-            let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
-            IntroAction (IntroApplyOn (c,(loc,pat))) in
+            let loc1 = Constrexpr_ops.constr_loc c in
+            let loc = Loc.merge loc0 loc1 in
+            IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in
           !@loc, List.fold_right f l pat ] ]
   ;
   simple_intropattern_closed:
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 75edf150e3..cd8c9e471e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -302,9 +302,9 @@ let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, _, id) -> Some id
 
-let add_glob_tactic_notation local n prods forml ids tac =
+let add_glob_tactic_notation local ~level prods forml ids tac =
   let parule = {
-    tacgram_level = n;
+    tacgram_level = level;
     tacgram_prods = prods;
   } in
   let tacobj = {
@@ -360,7 +360,7 @@ let extend_atomic_tactic name entries =
   in
   List.iteri add_atomic entries
 
-let add_ml_tactic_notation name prods =
+let add_ml_tactic_notation name ~level prods =
   let len = List.length prods in
   let iter i prods =
     let open Tacexpr in
@@ -372,10 +372,12 @@ let add_ml_tactic_notation name prods =
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
     let tac = TacML (Loc.ghost, entry, List.map map ids) in
-    add_glob_tactic_notation false 0 prods true ids tac
+    add_glob_tactic_notation false ~level prods true ids tac
   in
   List.iteri iter (List.rev prods);
-  extend_atomic_tactic name prods
+  (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
+  tactic_expr level 0) *)
+  if Int.equal level 0 then extend_atomic_tactic name prods
 
 (**********************************************************************)
 (** Ltac quotations                                                   *)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 969c118fb5..0695044736 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -45,7 +45,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
     to finding an argument by name (as in {!Genarg}) if there is none
     matching. *)
 
-val add_ml_tactic_notation : ml_tactic_name ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int ->
   argument grammar_tactic_prod_item_expr list list -> unit
 (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
     ML-side macro. *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 1a8f26b264..3f83f104e9 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -248,8 +248,8 @@ and intern_intro_pattern_action lf ist = function
   | IntroInjection l ->
       IntroInjection (List.map (intern_intro_pattern lf ist) l)
   | IntroWildcard | IntroRewrite _ as x -> x
-  | IntroApplyOn (c,pat) ->
-      IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
+  | IntroApplyOn ((loc,c),pat) ->
+      IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat)
 
 and intern_or_and_intro_pattern lf ist = function
    | IntroAndPattern l ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index aa646aa517..155cb31d85 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -520,7 +520,7 @@ let rec intropattern_ids (loc,pat) = match pat with
       List.flatten (List.map intropattern_ids (List.flatten ll))
   | IntroAction (IntroInjection l) ->
       List.flatten (List.map intropattern_ids l)
-  | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat
+  | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat
   | IntroNaming (IntroAnonymous | IntroFresh _)
   | IntroAction (IntroWildcard | IntroRewrite _)
   | IntroForthcoming _ -> []
@@ -913,14 +913,14 @@ and interp_intro_pattern_action ist env sigma = function
   | IntroInjection l ->
       let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
       sigma, IntroInjection l
-  | IntroApplyOn (c,ipat) ->
+  | IntroApplyOn ((loc,c),ipat) ->
       let c = { delayed = fun env sigma ->
         let sigma = Sigma.to_evar_map sigma in
         let (sigma, c) = interp_open_constr ist env sigma c in
         Sigma.Unsafe.of_pair (c, sigma)
       } in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
-      sigma, IntroApplyOn (c,ipat)
+      sigma, IntroApplyOn ((loc,c),ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
 
 and interp_or_and_intro_pattern ist env sigma = function
@@ -1422,7 +1422,14 @@ and tactic_of_value ist vle =
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
-  | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+  | VFun (_, _, _,vars,_) ->
+    let numargs = List.length vars in
+    Tacticals.New.tclZEROMSG
+      (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
+       Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
+       Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
+       pr_enum pr_name vars ++ Pp.str ".")
+  | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
     tactic_of_value ist tac
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index b09bdda65c..fe3a9f3b2a 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -51,8 +51,8 @@ let rec subst_intro_pattern subst = function
   | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x
 
 and subst_intro_pattern_action subst = function
-  | IntroApplyOn (t,pat) ->
-      IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat)
+  | IntroApplyOn ((loc,t),pat) ->
+      IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat)
   | IntroOrAndPattern l ->
       IntroOrAndPattern (subst_intro_or_and_pattern subst l)
   | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a2ffe12e93..88ea08c840 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -500,8 +500,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
 	     let open Pp in
-	     Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) 
-		 ++ fnl ()) in
+	     Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in
   match (flex_kind_of_term (fst ts) env evd term1 sk1, 
 	 flex_kind_of_term (fst ts) env evd term2 sk2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -1129,6 +1128,10 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in
   let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in
+  let () = if !debug_unification then
+	     let open Pp in
+	     Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1
+                                       ++ cut () ++ print_constr t2 ++ cut ())) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
   match kind_of_term term1, kind_of_term term2 with
   | Evar (evk1,args1), (Rel _|Var _) when app_empty
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 7b2c5695fd..360843711c 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -28,7 +28,7 @@ and pr_intro_pattern_action prc = function
   | IntroInjection pl ->
       str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
       str "]"
-  | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
+  | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
   | IntroRewrite true -> str "->"
   | IntroRewrite false -> str "<-"
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e698d1c72e..e56db4090a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1618,9 +1618,9 @@ end = struct (* {{{ *)
           Future.from_val (Option.get (Global.body_of_constant_body c)) in
         let uc =
           Future.chain
-            ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
-        let pr = Future.chain ~greedy:true ~pure:true pr discharge in
-        let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+            ~pure:true uc Univ.hcons_universe_context_set in
+        let pr = Future.chain ~pure:true pr discharge in
+        let pr = Future.chain ~pure:true pr Constr.hcons in
         Future.sink pr;
         let extra = Future.join uc in
         u.(bucket) <- uc;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6205bd1092..84d09d8330 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1815,24 +1815,37 @@ let find_matching_clause unifier clause =
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
 
+exception UnableToApply
+
 let progress_with_clause flags innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
-  if List.is_empty ordered_metas then error "Statement without assumptions.";
+  if List.is_empty ordered_metas then raise UnableToApply;
   let f mv =
     try Some (find_matching_clause (clenv_fchain ~with_univs:false mv ~flags clause) innerclause)
     with Failure _ -> None
   in
   try List.find_map f ordered_metas
-  with Not_found -> error "Unable to unify."
+  with Not_found -> raise UnableToApply
+
+let explain_unable_to_apply_lemma loc env sigma thm innerclause =
+  user_err ~loc (hov 0
+    (Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++
+     Pp.quote (Printer.pr_lconstr_env env sigma thm) ++ spc() ++
+     str "on hypothesis of type" ++ brk(1,1) ++
+     Pp.quote (Printer.pr_lconstr_env innerclause.env innerclause.evd (clenv_type innerclause)) ++
+     str "."))
 
-let apply_in_once_main flags innerclause env sigma (d,lbind) =
+let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
   let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
+    let e' = CErrors.push e in
     try aux (clenv_push_prod clause)
-    with NotExtensibleClause -> iraise e
+    with NotExtensibleClause ->
+      match e with
+      | UnableToApply -> explain_unable_to_apply_lemma loc env sigma thm innerclause
+      | _ -> iraise e'
   in
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
@@ -1852,7 +1865,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     try
-      let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
+      let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
       clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
         (fun id ->
           Tacticals.New.tclTHENLIST [
@@ -2467,7 +2480,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id =
       intro_decomp_eq loc l' thin tac id
   | IntroRewrite l2r ->
       rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
-  | IntroApplyOn (f,(loc,pat)) ->
+  | IntroApplyOn ((loc',f),(loc,pat)) ->
       let naming,tac_ipat =
         prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in
       let doclear =
@@ -2479,7 +2492,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id =
         let Sigma (c, sigma, p) = f.delayed env sigma in
         Sigma ((c, NoBindings), sigma, p)
       } in
-      apply_in_delayed_once false true true with_evars naming id (None,(loc,f))
+      apply_in_delayed_once false true true with_evars naming id (None,(loc',f))
         (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
 and prepare_intros_loc loc with_evars dft destopt = function
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
new file mode 100644
index 0000000000..ae3fd7acc7
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.out
@@ -0,0 +1,21 @@
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected:
+missing arguments for variables y and _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
new file mode 100644
index 0000000000..8ecd97aa56
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.v
@@ -0,0 +1,19 @@
+Ltac foo x := idtac x.
+Ltac bar x := fun y _ => idtac x y.
+Ltac baz := foo.
+Ltac qux := bar.
+Ltac mydo tac := tac ().
+Ltac rec x := rec.
+
+Goal True.
+  Fail foo.
+  Fail bar.
+  Fail bar True.
+  Fail baz.
+  Fail qux.
+  Fail mydo ltac:(fun _ _ => idtac).
+  Fail let tac := (fun _ => idtac) in tac.
+  Fail (fun _ => idtac).
+  Fail rec True.
+  Fail let rec tac x := tac in tac True.
+Abort.
\ No newline at end of file
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index fb1a7ab1c1..9b58c524e4 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -572,7 +572,8 @@ Proof.
   intros A P (x & Hp & Huniq); split.
   - intro; exists x; auto.
   - intros (x0 & HPx0 & HQx0) x1 HPx1.
-    replace x1 with x0 by (transitivity x; [symmetry|]; auto).
+    assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto).
+    destruct H.
     assumption.
 Qed.   
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 9fc00e80c1..2cc2ecbc20 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -103,7 +103,7 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P
     of an [a] of type [A], a of a proof [h] that [a] satisfies [P],
     and a proof [h'] that [a] satisfies [Q].  Then
     [(proj1_sig (sig_of_sig2 y))] is the witness [a],
-    [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and 
+    [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and
     [(proj3_sig y)] is the proof of [(Q a)]. *)
 
 Section Subset_projections2.
@@ -190,6 +190,23 @@ Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q
 Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q
   := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X).
 
+(** η Principles *)
+Definition sigT_eta {A P} (p : { a : A & P a })
+  : p = existT _ (projT1 p) (projT2 p).
+Proof. destruct p; reflexivity. Defined.
+
+Definition sig_eta {A P} (p : { a : A | P a })
+  : p = exist _ (proj1_sig p) (proj2_sig p).
+Proof. destruct p; reflexivity. Defined.
+
+Definition sigT2_eta {A P Q} (p : { a : A & P a & Q a })
+  : p = existT2 _ _ (projT1 (sigT_of_sigT2 p)) (projT2 (sigT_of_sigT2 p)) (projT3 p).
+Proof. destruct p; reflexivity. Defined.
+
+Definition sig2_eta {A P Q} (p : { a : A | P a & Q a })
+  : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p).
+Proof. destruct p; reflexivity. Defined.
+
 (** [sumbool] is a boolean type equipped with the justification of
     their value *)
 
@@ -263,10 +280,10 @@ Section Dependent_choice_lemmas.
     (forall x:X, {y | R x y}) ->
     forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
   Proof.
-    intros H x0. 
+    intros H x0.
     set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
     exists f.
-    split. reflexivity. 
+    split. reflexivity.
     induction n; simpl; apply proj2_sig.
   Defined.
 
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 56e03e965c..a10c180ccf 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -360,13 +360,12 @@ Module NoRetractToModalProposition.
 Section Paradox.
 
 Variable M : Prop -> Prop.
-Hypothesis unit : forall A:Prop, A -> M A.
-Hypothesis join : forall A:Prop, M (M A) -> M A.
 Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B.
 
 Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x).
 Proof.
-  eauto.
+  intros A P h x.
+  eapply incr in h; eauto.
 Qed.
 
 (** ** The universe of modal propositions *)
@@ -470,7 +469,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem paradox : forall B:NProp, El B.
 Proof.
   intros B.
-  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))).
   + exact (fun P => ~~P).
   + exact bool.
   + exact p2b.
@@ -480,8 +479,6 @@ Proof.
   + cbn. auto.
   + cbn. auto.
   + cbn. auto.
-  + auto.
-  + auto.
 Qed.
 
 End Paradox.
@@ -516,7 +513,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem mparadox : forall B:NProp, El B.
 Proof.
   intros B.
-  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))).
   + exact (fun P => P).
   + exact bool.
   + exact p2b.
@@ -526,8 +523,6 @@ Proof.
   + cbn. auto.
   + cbn. auto.
   + cbn. auto.
-  + auto.
-  + auto.
 Qed.
 
 End MParadox.
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index ef2709b472..8b0aa6691e 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -1,4 +1,5 @@
 Berardi.vo
+PropExtensionalityFacts.vo
 ChoiceFacts.vo
 ClassicalChoice.vo
 ClassicalDescription.vo
diff --git a/vernac/command.ml b/vernac/command.ml
index 049f58aa26..4b4f4d2711 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -81,7 +81,7 @@ let red_constant_entry n ce sigma = function
         let Sigma (c, _, _) = redfun.e_redfun env sigma c in
         c
       in
-      { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
+      { ce with const_entry_body = Future.chain ~pure:true proof_out
         (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
 
 let warn_implicits_in_term =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 55f33be399..798a238c74 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function
   (* Try all combinations... not optimal *)
      let env = Global.env() in
      { const with const_entry_body =
-        Future.chain ~greedy:true ~pure:true const.const_entry_body
+        Future.chain ~pure:true const.const_entry_body
         (fun ((body, ctx), eff) ->
           match kind_of_term body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8b7d654572..3afe04b37b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -517,9 +517,6 @@ let vernac_end_proof ?proof = function
   | Admitted          -> save_proof ?proof Admitted
   | Proved (_,_) as e -> save_proof ?proof e
 
-  (* A stupid macro that should be replaced by ``Exact c. Save.'' all along
-     the theories [??] *)
-
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)