From 5f9a9641c72b35650f62df43beb6f43f9f3a72e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 16 Oct 2015 16:41:58 +0200
Subject: Generalize fix for auto from PMP to eauto and typeclasses eauto.

---
 tactics/auto.ml          | 16 +++++++++-------
 tactics/auto.mli         |  3 +++
 tactics/class_tactics.ml | 42 +++++++++++++++++++++---------------------
 tactics/eauto.ml4        | 24 +++++++++++++-----------
 4 files changed, 46 insertions(+), 39 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 617c491c35..a6b53d76cc 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -72,16 +72,14 @@ let auto_flags_of_state st =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve poly flags ((c : raw_hint), clenv) =
-  Proofview.Goal.nf_enter begin fun gl ->
+let connect_hint_clenv poly (c, _, ctx) clenv gl =
   (** [clenv] has been generated by a hint-making function, so the only relevant
       data in its evarmap is the set of metas. The [evar_reset_evd] function
       below just replaces the metas of sigma by those coming from the clenv. *)
   let sigma = Proofview.Goal.sigma gl in
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (** Still, we need to update the universes *)
-  let (_, _, ctx) = c in
-  let clenv =
+  let clenv, c =
     if poly then
       (** Refresh the instance of the hint *)
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
@@ -91,11 +89,15 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
       (** FIXME: We're being inefficient here because we substitute the whole
           evar map instead of just its metas, which are the only ones
           mentioning the old universes. *)
-      Clenv.map_clenv map clenv
+      Clenv.map_clenv map clenv, map c
     else
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      { clenv with evd = evd ; env = Proofview.Goal.env gl }
-  in
+      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
+  in clenv, c
+		     
+let unify_resolve poly flags ((c : raw_hint), clenv) =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let clenv, c = connect_hint_clenv poly c clenv gl in
   let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
   Clenvtac.clenv_refine false clenv
   end
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 6e2acf7f56..cae180ce76 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -25,6 +25,9 @@ val default_search_depth : int ref
 
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
+val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
+			 [ `NF ] Proofview.Goal.t -> clausenv * constr
+						
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 36b60385d8..f3a4863444 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -154,33 +154,31 @@ let e_give_exact flags poly (c,clenv) gl =
     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
 
 let unify_e_resolve poly flags (c,clenv) gls =
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-  Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
+  let clenv', c = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine true ~with_classes:false clenv'
 
 let unify_resolve poly flags (c,clenv) gls =
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-  Proofview.V82.of_tactic 
-    (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
+  let clenv', _ = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine false ~with_classes:false clenv'
 
-let clenv_of_prods poly nprods (c, clenv) gls =
+let clenv_of_prods poly nprods (c, clenv) gl =
   let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some clenv
   else
-    let ty = pf_unsafe_type_of gls c in
+    let ty = Tacmach.New.pf_unsafe_type_of gl c in
     let diff = nb_prod ty - nprods in
       if Pervasives.(>=) diff 0 then
         (* Was Some clenv... *)
-	Some (mk_clenv_from_n gls (Some diff) (c,ty))
+	Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
       else None
 
-let with_prods nprods poly (c, clenv) f gls =
-  match clenv_of_prods poly nprods (c, clenv) gls with
-  | None -> tclFAIL 0 (str"Not enough premisses") gls
-  | Some clenv' -> f (c, clenv') gls
+let with_prods nprods poly (c, clenv) f =
+  Proofview.Goal.nf_enter (fun gl ->
+  match clenv_of_prods poly nprods (c, clenv) gl with
+  | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+  | Some clenv' -> f (c, clenv') gl)
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 
@@ -224,12 +222,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
       let tac = function
-      | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
-      | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+      | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
+      | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
       | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
       | Res_pf_THEN_trivial_fail (term,cl) ->
-          Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
-            (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+         Proofview.V82.tactic (tclTHEN
+				 (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags))))
+				 (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
       | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
       | Extern tacast -> conclPattern concl p tacast
       in
@@ -847,4 +846,5 @@ let autoapply c i gl =
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
   let cty = pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  unify_e_resolve false flags (c,ce) gl
+  let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in
+  Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 09c5fa873f..ca430ec111 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -116,15 +116,17 @@ open Unification
 (***************************************************************************)
 
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
-
-let unify_e_resolve poly flags (c,clenv) gls =
-  let (c, _, _) = c in
-  let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv 
-  else clenv, Univ.empty_level_subst in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-    tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-      (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
+			  
+let unify_e_resolve poly flags (c,clenv) =
+  Proofview.Goal.nf_enter begin
+      fun gl ->
+      let clenv', c = connect_hint_clenv poly c clenv gl in
+      Proofview.V82.tactic
+	(fun gls ->
+	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
+	 tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+    end
 
 let hintmap_of hdc concl =
   match hdc with
@@ -166,10 +168,10 @@ and e_my_find_search db_list local_db hdc concl =
       (b,
         let tac = function
         | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
-        | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
+        | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
         | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl))
         | Res_pf_THEN_trivial_fail (term,cl) ->
-          Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl))
+          Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl)))
             (e_trivial_fail_db db_list local_db))
         | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
         | Extern tacast -> conclPattern concl p tacast
-- 
cgit v1.2.3


From 3664fd9f0af7851ed35e1fc06d826f7fd8ee2f7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Oct 2015 12:00:12 +0200
Subject: Test for bug #4325.

---
 test-suite/bugs/closed/4325.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 test-suite/bugs/closed/4325.v

diff --git a/test-suite/bugs/closed/4325.v b/test-suite/bugs/closed/4325.v
new file mode 100644
index 0000000000..af69ca04b6
--- /dev/null
+++ b/test-suite/bugs/closed/4325.v
@@ -0,0 +1,5 @@
+Goal (forall a b : nat, Set = (a = b)) -> Set.
+Proof.
+  clear.
+  intro H.
+  erewrite (fun H' => H _ H').
-- 
cgit v1.2.3


From 28297a3994779fda9b9208cb90bd6f8f08d652c5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Oct 2015 12:35:25 +0200
Subject: Lemmas accept the Local flag.

This was a trivial overlook.
---
 toplevel/vernacentries.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f1f87ca9b1..d04d6c9eda 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -478,7 +478,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
  		Some (snd (interp_redexp env evc r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
-let vernac_start_proof p kind l lettop =
+let vernac_start_proof locality p kind l lettop =
+  let local = enforce_locality_exp locality None in
   if Dumpglob.dump () then
     List.iter (fun (id, _) ->
       match id with
@@ -488,7 +489,7 @@ let vernac_start_proof p kind l lettop =
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
-  start_proof_and_print (Global, p, Proof kind) l no_hook
+  start_proof_and_print (local, p, Proof kind) l no_hook
 
 let qed_display_script = ref true
 
@@ -1860,7 +1861,7 @@ let interp ?proof ~loc locality poly c =
 
   (* Gallina *)
   | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
-  | VernacStartTheoremProof (k,l,top) -> vernac_start_proof poly k l top
+  | VernacStartTheoremProof (k,l,top) -> vernac_start_proof locality poly k l top
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
@@ -1965,7 +1966,7 @@ let interp ?proof ~loc locality poly c =
   | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm")
   
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false
+  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()
@@ -2006,7 +2007,7 @@ let check_vernac_supports_locality c l =
     | VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
-    | VernacAssumption _
+    | VernacAssumption _ | VernacStartTheoremProof _
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
     | VernacDeclareMLModule _
-- 
cgit v1.2.3


From 14edc57ac5ad75bbc4ea8559111606aea8978f48 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 18 Oct 2015 19:35:57 +0200
Subject: Adding a function to mirror decompose_prod_n_assum in that it counts
 let-ins, to compensate decompose_lam_n_assum which does not count let-ins.

Any idea on a uniform and clear naming scheme for this kind of
decomposition functions?
---
 kernel/term.ml  | 28 +++++++++++++++++++++++-----
 kernel/term.mli | 31 ++++++++++++++++++++-----------
 2 files changed, 43 insertions(+), 16 deletions(-)

diff --git a/kernel/term.ml b/kernel/term.ml
index 7bf4c8182d..33ed25fe1b 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -566,8 +566,10 @@ let decompose_lam_assum =
   in
   lamdec_rec empty_rel_context
 
-(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T
-   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+(* Given a positive integer n, decompose a product or let-in term
+   of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair
+   of the quantifying context [(xn,None,Tn);..;(xi,Some
+   ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *)
 let decompose_prod_n_assum n =
   if n < 0 then
     error "decompose_prod_n_assum: integer parameter must be positive";
@@ -581,10 +583,12 @@ let decompose_prod_n_assum n =
   in
   prodec_rec empty_rel_context n
 
-(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
-   into the pair ([(xn,Tn);...;(x1,T1)],T)
+(* Given a positive integer n, decompose a lambda or let-in term [fun
+   (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted
+   context [(xn,None,Tn);...;(xi,Some ci,Ti);...;(x1,None,T1)] and of
+   the inner body [T].
    Lets in between are not expanded but turn into local definitions,
-   but n is the actual number of destructurated lambdas.  *)
+   but n is the actual number of destructurated lambdas. *)
 let decompose_lam_n_assum n =
   if n < 0 then
     error "decompose_lam_n_assum: integer parameter must be positive";
@@ -598,6 +602,20 @@ let decompose_lam_n_assum n =
   in
   lamdec_rec empty_rel_context n
 
+(* Same, counting let-in *)
+let decompose_lam_n_decls n =
+  if n < 0 then
+    error "decompose_lam_n_decls: integer parameter must be positive";
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else match kind_of_term c with
+    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | Cast (c,_,_)      -> lamdec_rec l n c
+    | c -> error "decompose_lam_n_decls: not enough abstractions"
+  in
+  lamdec_rec empty_rel_context n
+
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
 let nb_lam =
diff --git a/kernel/term.mli b/kernel/term.mli
index 501aaf741e..d60716410c 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -281,13 +281,15 @@ val decompose_prod : constr -> (Name.t*constr) list * constr
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *)
 val decompose_lam : constr -> (Name.t*constr) list * constr
 
-(** Given a positive integer n, transforms a product term
+(** Given a positive integer n, decompose a product term
    {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %}
-   into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *)
+   into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}.
+   Raise a user error if not enough products. *)
 val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr
 
-(** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term
-   {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *)
+(** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term
+   {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}.
+   Raise a user error if not enough lambdas. *)
 val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
@@ -297,10 +299,15 @@ val decompose_prod_assum : types -> rel_context * types
 (** Idem with lambda's *)
 val decompose_lam_assum : constr -> rel_context * constr
 
-(** Idem but extract the first [n] premisses *)
+(** Idem but extract the first [n] premisses, counting let-ins. *)
 val decompose_prod_n_assum : int -> types -> rel_context * types
+
+(** Idem for lambdas, _not_ counting let-ins *)
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
 
+(** Idem, counting let-ins *)
+val decompose_lam_n_decls : int -> constr -> rel_context * constr
+
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
 val nb_lam : constr -> int
@@ -308,12 +315,14 @@ val nb_lam : constr -> int
 (** Similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
-(** Returns the premisses/parameters of a type/term (let-in included) *)
+(** Return the premisses/parameters of a type/term (let-in included) *)
 val prod_assum : types -> rel_context
 val lam_assum : constr -> rel_context
 
-(** Returns the first n-th premisses/parameters of a type/term (let included)*)
+(** Return the first n-th premisses/parameters of a type (let included and counted) *)
 val prod_n_assum : int -> types -> rel_context
+
+(** Return the first n-th premisses/parameters of a term (let included but not counted) *)
 val lam_n_assum : int -> constr -> rel_context
 
 (** Remove the premisses/parameters of a type/term *)
@@ -328,11 +337,11 @@ val strip_lam_n : int -> constr -> constr
 val strip_prod_assum : types -> types
 val strip_lam_assum : constr -> constr
 
-(** flattens application lists *)
+(** Flattens application lists *)
 val collapse_appl : constr -> constr
 
 
-(** Removes recursively the casts around a term i.e.
+(** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
 val strip_outer_cast : constr -> constr
 
@@ -352,10 +361,10 @@ type arity = rel_context * sorts
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types
 
-(** Destructs an "arity" into its canonical form *)
+(** Destruct an "arity" into its canonical form *)
 val destArity : types -> arity
 
-(** Tells if a term has the form of an arity *)
+(** Tell if a term has the form of an arity *)
 val isArity : types -> bool
 
 (** {5 Kind of type} *)
-- 
cgit v1.2.3


From 23545b802a14b2fad10f4382604c71f55b7d6d0e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 18 Oct 2015 19:44:49 +0200
Subject: Using appropriate lambda decomposition function counting let-ins when
 dealing with "match".

Contrastingly, "fix" is considered not to count let-ins for finding
the recursive argument (which is ok because the last argument is
necessarily a lambda).
---
 pretyping/cases.ml           | 5 +++--
 pretyping/constr_matching.ml | 4 ++--
 pretyping/detyping.ml        | 2 +-
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 47d92f5e03..a5a7ace221 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1077,7 +1077,7 @@ let rec ungeneralize n ng body =
         let p = prod_applist p [mkRel (n+List.length sign+ng)] in
         it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
       mkCase (ci,p,c,Array.map2 (fun q c ->
-        let sign,b = decompose_lam_n_assum q c in
+        let sign,b = decompose_lam_n_decls q c in
         it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign)
         ci.ci_cstr_ndecls brs)
   | App (f,args) ->
@@ -1102,7 +1102,8 @@ let rec is_dependent_generalization ng body =
   | Case (ci,p,c,brs) ->
       (* We traverse a split *)
       Array.exists2 (fun q c ->
-        let _,b = decompose_lam_n_assum q c in is_dependent_generalization ng b)
+        let _,b = decompose_lam_n_decls q c in
+        is_dependent_generalization ng b)
         ci.ci_cstr_ndecls brs
   | App (g,args) ->
       (* We traverse an inner generalization *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 121ab74885..5e99521a12 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -267,8 +267,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
-	  let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
-	  let ctx_b2',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
+	  let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in
+	  let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in
 	  let n = rel_context_length ctx_b2 in
           let n' = rel_context_length ctx_b2' in
 	  if noccur_between 1 n b2 && noccur_between 1 n' b2' then
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a1213e72be..87f2550240 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -302,7 +302,7 @@ and contract_branch isgoal e (cdn,can,mkpat,b) =
 let is_nondep_branch c l =
   try
     (* FIXME: do better using tags from l *)
-    let sign,ccl = decompose_lam_n_assum (List.length l) c in
+    let sign,ccl = decompose_lam_n_decls (List.length l) c in
     noccur_between 1 (rel_context_length sign) ccl
   with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
-- 
cgit v1.2.3


From 8748947349a206a502e43cfe70e3397ee457c4f7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 17 Oct 2015 17:26:38 +0200
Subject: Fixing #4198 (continued): not matching within the inner
 lambdas/let-ins of the return clause and of the branches (what assumed that
 the implementation preserves the invariant that the return predicate and the
 branches are in canonical [fun Δ => t] form, with Δ possibly containing
 let-ins).

---
 pretyping/constr_matching.ml | 19 ++++++++++++++++---
 test-suite/success/ltac.v    | 26 ++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5e99521a12..3fa037ffdd 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -413,12 +413,25 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
           let sub = (env, c1) :: subargs env lc in
           try_aux sub mk_ctx next
-  | Case (ci,hd,c1,lc) ->
+  | Case (ci,p,c,brs) ->
+      (* Warning: this assumes predicate and branches to be
+         in canonical form using let and fun of the signature *)
+      let nardecls = List.length ci.ci_pp_info.ind_tags in
+      let sign_p,p = decompose_lam_n_decls (nardecls + 1) p in
+      let env_p = Environ.push_rel_context sign_p env in
+      let brs = Array.map2 decompose_lam_n_decls ci.ci_cstr_ndecls brs in
+      let sign_brs = Array.map fst brs in
+      let f (sign,br) = (Environ.push_rel_context sign env, br) in
+      let sub_br = Array.map f brs in
       let next_mk_ctx = function
-      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | c :: p :: brs ->
+        let p = it_mkLambda_or_LetIn p sign_p in
+        let brs =
+          Array.map2 it_mkLambda_or_LetIn (Array.of_list brs) sign_brs in
+        mk_ctx (mkCase (ci,p,c,brs))
       | _ -> assert false
       in
-      let sub = (env, c1) :: (env, hd) :: subargs env lc in
+      let sub = (env, c) :: (env_p, p) :: Array.to_list sub_br in
       try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 6c4d4ae98f..5bef2e512a 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,29 @@ let T := constr:(fun a b : nat => a) in
   end.
 exact (eq_refl n).
 Qed.
+
+(* Check that matching "match" does not look into the invisible
+   canonically generated binders of the return clause and of the branches *)
+
+Goal forall n, match n with 0 => true | S _ => false end = true.
+intros. unfold nat_rect.
+Fail match goal with |- context [nat] => idtac end.
+Abort.
+
+(* Check that branches of automatically generated elimination
+   principle are correctly eta-expanded and hence matchable as seen
+   from the user point of view *)
+
+Goal forall a f n, nat_rect (fun _ => nat) a f n = 0.
+intros. unfold nat_rect.
+match goal with |- context [f _] => idtac end.
+Abort.
+
+(* Check that branches of automatically generated elimination
+   principle are in correct form also in the presence of let-ins *)
+
+Inductive a (b:=0) : let b':=1 in Type := c : let d:=0 in a.
+Goal forall x, match x with c => 0 end = 1.
+intros.
+match goal with |- context [0] => idtac end.
+Abort.
-- 
cgit v1.2.3


From a856dfb5ce98ea1a8e3961a64e533565387a8b31 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Oct 2015 19:37:55 +0200
Subject: Reference Manual: Applying standard style recommendation about not
 starting a sentence with a symbolic expression.

---
 doc/refman/RefMan-ltac.tex | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 04c356e44f..5880487f71 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -367,7 +367,8 @@ There is a for loop that repeats a tactic {\num} times:
 \begin{quote}
 {\tt do} {\num} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+This tactic value $v$ is
 applied {\num} times. Supposing ${\num}>1$, after the first
 application of $v$, $v$ is applied, at least once, to the generated
 subgoals and so on. It fails if the application of $v$ fails before
@@ -394,7 +395,8 @@ We can catch the tactic errors with:
 \begin{quote}
 {\tt try} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied to each focused goal independently. If the application of $v$
 fails in a goal, it catches the error and leaves the goal
 unchanged. If the level of the exception is positive, then the
@@ -406,7 +408,8 @@ We can check if a tactic made progress with:
 \begin{quote}
 {\tt progress} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied to each focued subgoal independently. If the application of
 $v$ to one of the focused subgoal produced subgoals equal to the
 initial goals (up to syntactical equality), then an error of level 0
@@ -422,7 +425,7 @@ We can branch with the following structure:
 {\tacexpr}$_1$ {\tt +} {\tacexpr}$_2$
 \end{quote}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
-$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied to each
+$v_2$ which must be tactic values. The tactic value $v_1$ is applied to each
 focused goal independently and if it fails or a later tactic fails,
 then the proof backtracks to the current goal and $v_2$ is applied.
 
@@ -462,7 +465,7 @@ Yet another way of branching without backtracking is the following structure:
 {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
 \end{quote}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
-$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied in each
+$v_2$ which must be tactic values. The tactic value $v_1$ is applied in each
 subgoal independently and if it fails \emph{to progress} then $v_2$ is
 applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt
   first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress}
@@ -494,7 +497,8 @@ single success \emph{a posteriori}:
 \begin{quote}
 {\tt once} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied but only its first success is used. If $v$ fails, {\tt once}
 {\tacexpr} fails like $v$. If $v$ has a least one success, {\tt once}
 {\tacexpr} succeeds once, but cannot produce more successes.
@@ -505,7 +509,8 @@ Coq provides an experimental way to check that a tactic has \emph{exactly one} s
 \begin{quote}
 {\tt exactly\_once} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied if it has at most one success. If $v$ fails, {\tt
   exactly\_once} {\tacexpr} fails like $v$. If $v$ has a exactly one
 success, {\tt exactly\_once} {\tacexpr} succeeds like $v$. If $v$ has
@@ -592,7 +597,8 @@ amount of time:
 \begin{quote}
 {\tt timeout} {\num} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied normally, except that it is interrupted after ${\num}$ seconds
 if it is still running. In this case the outcome is a failure.
 
-- 
cgit v1.2.3


From c70ee60ed1603658eb33f4ae39b1a0be81bf45c6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 17 Oct 2015 17:29:19 +0200
Subject: Using "__" rather than this unelegant arbitrary "A" for the name of
 variables of the context of an evar in debugging mode.

---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 87f2550240..b5228094a2 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -513,7 +513,7 @@ let rec detype flags avoid env sigma t =
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
-          (Array.map_to_list (fun c -> (Id.of_string "A",c)) cl)
+          (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
       in
         GEvar (dl,id,
                List.map (on_snd (detype flags avoid env sigma)) l)
-- 
cgit v1.2.3


From c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Oct 2015 11:40:22 +0200
Subject: Miscellaneous typos, spacing, US spelling in comments or variable
 names.

---
 kernel/typeops.ml       | 2 +-
 lib/future.mli          | 4 ++--
 proofs/logic_monad.ml   | 2 +-
 proofs/proof_global.mli | 2 +-
 stm/stm.ml              | 4 ++--
 toplevel/coqtop.mli     | 2 +-
 6 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 09299f31d7..4f32fdce83 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -477,7 +477,7 @@ let rec execute env cstr =
       let j' = execute env1 c3 in
         judge_of_letin env name j1 j2 j'
 
-    | Cast (c,k, t) ->
+    | Cast (c,k,t) ->
       let cj = execute env c in
       let tj = execute_type env t in
         judge_of_cast env cj k tj
diff --git a/lib/future.mli b/lib/future.mli
index de2282ae92..adc15e49c7 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -91,13 +91,13 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
  * When a future enters the environment a corresponding hook is run to perform
  * some work.  If this fails, then its failure has to be annotated with the
  * same state id that corresponds to the future computation end.  I.e. Qed
- * is split into two parts, the lazy one (the future) and the eagher one
+ * is split into two parts, the lazy one (the future) and the eager one
  * (the hook), both performing some computations for the same state id. *)
 val fix_exn_of : 'a computation -> fix_exn
 
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
-   delage assigns it. *)
+   delegate assigns it. *)
 type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
   ?blocking:bool -> name:string ->
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 81f02b66db..b9165aa812 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -188,7 +188,7 @@ struct
       shape of the monadic type is reminiscent of that of the
       continuation monad transformer.
 
-      The paper also contains the rational for the [split] abstraction.
+      The paper also contains the rationale for the [split] abstraction.
 
       An explanation of how to derive such a monad from mathematical
       principles can be found in "Kan Extensions for Program
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 028116049c..fcb706cc8d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -94,7 +94,7 @@ val start_dependent_proof :
 val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
- * Both access the current proof state. The formes is supposed to be
+ * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
diff --git a/stm/stm.ml b/stm/stm.ml
index 5bb46fd368..88a1fbbf48 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -639,7 +639,7 @@ end = struct (* {{{ *)
     proof,
     Summary.project_summary (States.summary_of_state system) summary_pstate
 
-  let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
+  let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
 
   let is_cached ?(cache=`No) id =
     if Stateid.equal id !cur_id then
@@ -1912,7 +1912,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline "Initialising workers";
+    prerr_endline "Initializing workers";
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 356ccdcc69..6704474529 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -8,7 +8,7 @@
 
 (** The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input
-   state, load the files given on the command line, load the ressource file,
+   state, load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
 val init_toplevel : string list -> unit
-- 
cgit v1.2.3


From 289dde7331ee19229b9ba4b9778a76007d93b275 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Oct 2015 10:55:19 +0200
Subject: Documenting the option "Strict Universe Declaration" in CHANGES.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index 07d129a462..9f46131363 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,9 @@ Vernacular commands
 
 - New command "Redirect" to redirect the output of a command to a file.
 - New command "Undelimit Scope" to remove the delimiter of a scope.
+- New option "Strict Universe Declaration", set by default. It enforces the
+  declaration of all polymorphic universes appearing in a definition when
+  introducing it.
 
 Tactics
 
-- 
cgit v1.2.3


From de32427bd2785c365374c554b4b74e97749cb995 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 19 Oct 2015 11:28:30 +0200
Subject: Fixed #4274, bad formatting of messages in emacs mode.

---
 lib/pp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/pp.ml b/lib/pp.ml
index 1711008ead..4ed4b17791 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -362,11 +362,11 @@ let emacs_quote_info_start = "<infomsg>"
 let emacs_quote_info_end = "</infomsg>"
 
 let emacs_quote g =
-  if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end
+  if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
   else hov 0 g
 
 let emacs_quote_info g =
-  if !print_emacs then str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end
+  if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
   else hov 0 g
 
 
-- 
cgit v1.2.3


From 70d3ad33f6ba7a1c6b1fb93aadd5c05d7e9c03b8 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 19 Oct 2015 11:49:38 +0200
Subject: Partly fixes #3225. Removed some old experimental stuff in funind.

---
 plugins/funind/g_indfun.ml4 | 244 --------------------------------------------
 1 file changed, 244 deletions(-)

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e7732a5037..045beb37cf 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -247,247 +247,3 @@ END
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 ["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ]
 END
-
-
-
-
-
-(* FINDUCTION *)
-
-(* comment this line to see debug msgs *)
-let msg x = () ;; let pr_lconstr c = str ""
-  (* uncomment this to see debugging *)
-let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
-let prNamedConstr s c =
-  begin
-    msg(str "");
-    msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
-    msg(str "");
-  end
-
-
-
-(** Information about an occurrence of a function call (application)
-    inside a term. *)
-type fapp_info = {
-  fname: constr; (** The function applied *)
-  largs: constr list; (** List of arguments *)
-  free: bool; (** [true] if all arguments are debruijn free *)
-  max_rel: int; (** max debruijn index in the funcall *)
-  onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
-}
-
-
-(** [constr_head_match(a b c) a] returns true, false otherwise. *)
-let constr_head_match u t=
-  if isApp u
-  then
-    let uhd,args= destApp u in
-    Constr.equal uhd t
-  else false
-
-(** [hdMatchSub inu t] returns the list of occurrences of [t] in
-    [inu]. DeBruijn are not pushed, so some of them may be unbound in
-    the result. *)
-let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
-  let subres =
-    match kind_of_term inu with
-      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) ->
-	  hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
-      | Fix (_,(lna,tl,bl))  -> (* not sure Fix is correct *)
-	  Array.fold_left
-	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test)
-	    [] bl
-      | _ -> (* Cofix will be wrong *)
-	  fold_constr
-	    (fun l cstr ->
-	      l @ hdMatchSub cstr test) [] inu in
-  if not (test inu) then subres
-  else
-    let f,args = decompose_app inu in
-    let freeset = Termops.free_rels inu in
-    let max_rel = try Int.Set.max_elt freeset with Not_found -> -1 in
-    {fname = f; largs = args; free = Int.Set.is_empty freeset;
-    max_rel = max_rel; onlyvars = List.for_all isVar args }
-    ::subres
-
-let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-
-let mkEq typ c1 c2 =
-  mkApp (make_eq(),[| typ; c1; c2|])
-
-
-let poseq_unsafe idunsafe cstr gl =
-  let typ = Tacmach.pf_unsafe_type_of gl cstr in
-  tclTHEN
-    (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl))
-    (tclTHENFIRST
-      (Proofview.V82.of_tactic (Tactics.assert_before Anonymous (mkEq typ (mkVar idunsafe) cstr)))
-      (Proofview.V82.of_tactic Tactics.reflexivity))
-    gl
-
-
-let poseq id cstr gl =
-  let x = Tactics.fresh_id [] id gl in
-  poseq_unsafe x cstr gl
-
-(* dirty? *)
-
-let list_constr_largs = ref []
-
-let rec poseq_list_ids_rec lcstr gl =
-  match lcstr with
-    | [] -> tclIDTAC gl
-    | c::lcstr' ->
-	match kind_of_term c with
-	  | Var _ ->
-	      (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
-	  | _ ->
-	      let _ = prstr "c = " in
-	      let _ = prconstr c in
-	      let _ = prstr "\n" in
-	      let typ = Tacmach.pf_unsafe_type_of gl c in
-	      let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in
-	      let x = Tactics.fresh_id [] cname gl in
-	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
-	      let _ = prstr " list_constr_largs = " in
-	      let _ = prlistconstr !list_constr_largs in
-	      let _ = prstr "\n" in
-
-	      tclTHEN
-		(poseq_unsafe x c)
-		(poseq_list_ids_rec lcstr')
-		gl
-
-let poseq_list_ids lcstr gl =
-  let _ = list_constr_largs := [] in
-  poseq_list_ids_rec lcstr gl
-
-(** [find_fapp test g] returns the list of [app_info] of all calls to
-    functions that satisfy [test] in the conclusion of goal g. Trivial
-    repetition (not modulo conversion) are deleted. *)
-let find_fapp (test:constr -> bool) g : fapp_info list =
-  let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
-  let res =
-    List.fold_right (List.add_set Pervasives.(=)) pre_res [] in
-  (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
-  res)
-
-
-
-(** [finduction id filter g] tries to apply functional induction on
-    an occurrence of function [id] in the conclusion of goal [g]. If
-    [id]=[None] then calls to any function are selected. In any case
-    [heuristic] is used to select the most pertinent occurrence. *)
-let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
-    (nexttac:Proof_type.tactic) g =
-  let test = match oid with
-    | Some id ->
-       let idref = const_of_id id in
-       (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *)
-       let idconstr = snd (Evd.fresh_global (Global.env ()) (Evd.from_env (Global.env ())) idref) in
-	(fun u -> constr_head_match u idconstr) (* select only id *)
-    | None -> (fun u -> isApp u) in (* select calls to any function *)
-  let info_list = find_fapp test g in
-  let ordered_info_list = heuristic info_list in
-  prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
-  if List.is_empty ordered_info_list then Errors.error "function not found in goal\n";
-  let taclist: Proof_type.tactic list =
-    List.map
-      (fun info ->
-	(tclTHEN
-	  (tclTHEN (poseq_list_ids info.largs)
-	    (
-	      fun gl ->
-		  (functional_induction
-		    true (applist (info.fname, List.rev !list_constr_largs))
-		    None None) gl))
-	  nexttac)) ordered_info_list in
-  (* we try each (f t u v) until one does not fail *)
-  (* TODO: try also to mix functional schemes *)
-  tclFIRST taclist g
-
-
-
-
-(** [chose_heuristic oi x] returns the heuristic for reordering
-    (and/or forgetting some elts of) a list of occurrences of
-     function calls infos to chose first with functional induction. *)
-let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
-  match oi with
-    | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
-    | None ->
-	(* Default heuristic: put first occurrences where all arguments
-	   are *bound* (meaning already introduced) variables *)
-	let ordering x y =
-	  if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
-	  else if x.free && x.onlyvars then -1
-	  else if y.free && y.onlyvars then 1
-	  else 0 (* both not pertinent *)
-	in
-	List.sort ordering
-
-
-
-TACTIC EXTEND finduction
-    ["finduction" ident(id) natural_opt(oi)] ->
-      [
-	match oi with
-	  | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0"
-	  | _ ->
-	      let heuristic = chose_heuristic oi in
-	      Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC)
-      ]
-END
-
-
-
-TACTIC EXTEND fauto
-    [ "fauto" tactic(tac)] ->
-      [
-	let heuristic = chose_heuristic None in
-	Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac)))
-      ]
-  |
-    [ "fauto" ] ->
-      [
-	let heuristic = chose_heuristic None in
-	Proofview.V82.tactic (finduction None heuristic tclIDTAC)
-      ]
-
-END
-
-
-TACTIC EXTEND poseq
-  [ "poseq" ident(x) constr(c) ] ->
-      [ Proofview.V82.tactic (poseq x c) ]
-END
-
-VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY
-  [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
-END
-
-VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
-  [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
-      "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
-     [
-       let f1,ctx = Constrintern.interp_constr (Global.env()) Evd.empty
-	 (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
-       let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty
-	 (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
-       let f1type = Typing.unsafe_type_of (Global.env()) Evd.empty f1 in
-       let f2type = Typing.unsafe_type_of (Global.env()) Evd.empty f2 in
-       let ar1 = List.length (fst (decompose_prod f1type)) in
-       let ar2 = List.length (fst (decompose_prod f2type)) in
-       let _ =
-	 if not (Int.equal ar1 (List.length cl1)) then
-	   Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in
-       let _ =
-	 if not (Int.equal ar2 (List.length cl2)) then
-	   Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in
-       Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
-     ]
-END
-- 
cgit v1.2.3


From c3967bd7a71df53a004478d23b072309f13f2ff5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Oct 2015 16:06:46 +0200
Subject: Turning anomaly into error for #4372 (weakness of inversion in the
 presence of dependent types with only superficial dependency).

See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372.
---
 tactics/equality.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5ed9ac2ba0..bc711b81ef 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1126,7 +1126,14 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
-	| None -> anomaly (Pp.str "Not enough components to build the dependent tuple")
+	| None ->
+            (* This at least happens if what has been detected as a
+               dependency is not one; use an evasive error message;
+               even if the problem is upwards: unification should be
+               tried in the first place in make_iterated_tuple instead
+               of approximatively computing the free rels; then
+               unsolved evars would mean not binding rel *)
+	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
     !evdref, Evarutil.nf_evar !evdref scf
-- 
cgit v1.2.3


From b3b04d0a5c7c39140e2125321a17957ddcaf2b33 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Oct 2015 17:23:48 +0200
Subject: Test for #4372 (anomaly in inversion in the presence of fake
 dependency).

---
 test-suite/bugs/closed/4372.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/bugs/closed/4372.v

diff --git a/test-suite/bugs/closed/4372.v b/test-suite/bugs/closed/4372.v
new file mode 100644
index 0000000000..428192a344
--- /dev/null
+++ b/test-suite/bugs/closed/4372.v
@@ -0,0 +1,20 @@
+(* Tactic inversion was raising an anomaly because of a fake
+   dependency of TypeDenote into its argument *)
+
+Inductive expr :=
+| ETrue.
+
+Inductive IntermediateType : Set := ITbool.
+
+Definition TypeDenote (IT : IntermediateType) : Type :=
+  match IT with
+  | _ => bool
+  end.
+
+Inductive ValueDenote : forall (e:expr) it, TypeDenote it -> Prop :=
+| VT : ValueDenote ETrue ITbool true.
+
+Goal forall it v, @ValueDenote ETrue it v -> True.
+  intros it v H.
+  inversion H.
+Abort.
-- 
cgit v1.2.3


From 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 19 Oct 2015 18:12:27 +0200
Subject: Categorizing debug messages as such + NonLogical uses loggers.

---
 proofs/logic_monad.ml  | 15 +++++++--------
 proofs/logic_monad.mli |  9 +++++----
 proofs/tactic_debug.ml |  6 +++---
 tactics/tacinterp.ml   |  6 +++---
 4 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index b9165aa812..e3caa886a2 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -94,14 +94,6 @@ struct
 
   let print_char = fun c -> (); fun () -> print_char c
 
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  let print_debug = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
-    let (e, info) = Errors.push e in raise ~info e ()
-
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.msg_notice s; Pp.pp_flush () with e ->
-    let (e, info) = Errors.push e in raise ~info e ()
-
   let timeout = fun n t -> (); fun () ->
     Control.timeout n t (Exception Timeout)
 
@@ -111,6 +103,13 @@ struct
       let (e, info) = Errors.push e in
       Util.iraise (Exception e, info)
 
+  (** Use the current logger. The buffer is also flushed. *)
+  let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
+  let print_info s =  make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
+  let print_warning s =  make (fun _ -> Pp.msg_warning s;Pp.pp_flush ())
+  let print_error s =  make (fun _ -> Pp.msg_error s;Pp.pp_flush ())
+  let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ())
+
   let run = fun x ->
     try x () with Exception e as src ->
       let (src, info) = Errors.push src in
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index 511dd7a6ed..84ffda7533 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -55,12 +55,13 @@ module NonLogical : sig
 
   val read_line : string t
   val print_char : char -> unit t
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  val print : Pp.std_ppcmds -> unit t
 
-  (* FIXME: shouldn't we have a logger instead? *)
-  (** {!Pp.pp}. The buffer is also flushed. *)
+  (** Loggers. The buffer is also flushed. *)
   val print_debug : Pp.std_ppcmds -> unit t
+  val print_warning : Pp.std_ppcmds -> unit t
+  val print_notice : Pp.std_ppcmds -> unit t
+  val print_info : Pp.std_ppcmds -> unit t
+  val print_error : Pp.std_ppcmds -> unit t
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 667765dbf2..6d6215c521 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -33,7 +33,7 @@ let explain_logic_error = ref (fun e -> mt())
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
 let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
-let msg_tac_notice s = Proofview.NonLogical.print (s++fnl())
+let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
 
 (* Prints the goal *)
 
@@ -122,7 +122,7 @@ let run ini =
   let open Proofview.NonLogical in
   if not ini then
     begin
-      Proofview.NonLogical.print (str"\b\r\b\r") >>
+      Proofview.NonLogical.print_notice (str"\b\r\b\r") >>
       !skipped >>= fun skipped ->
       msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl())
     end >>
@@ -137,7 +137,7 @@ let rec prompt level =
   let runtrue = run true in
   begin
     let open Proofview.NonLogical in
-    Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+    Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 96d0b592b8..5a0d26a1cb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,8 +44,8 @@ open Proofview.Notations
 
 let safe_msgnl s =
   Proofview.NonLogical.catch
-    (Proofview.NonLogical.print (s++fnl()))
-    (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl()))
+    (Proofview.NonLogical.print_debug (s++fnl()))
+    (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl()))
 
 type value = tlevel generic_argument
 
@@ -1136,7 +1136,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         interp_message ist s >>= fun msg ->
         return (hov 0 msg , hov 0 msg)
       in
-      let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in
+      let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in
       let log (msg,_) = Proofview.Trace.log (fun () -> msg) in
       let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in
       Ftactic.run msgnl begin fun msgnl ->
-- 
cgit v1.2.3