Merge branch 'v8.5'

24 files changed, 140 insertions, 78 deletions

diff --git a/CHANGES b/CHANGES
index 9108c1454..a77889fc4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -128,8 +128,6 @@ API
 
 - The interface of [change] has changed to take a [change_arg], which
   can be built from a [constr] using [make_change_arg].
-- [pattern_of_constr] now returns a triplet including the cleaned-up
-  [evar_map], removing the evars that were turned into metas.
 
 Changes from V8.4 to V8.5beta1
 ==============================
diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5
index 2ca62e3d7..ebbc05773 100644
--- a/dev/doc/README-V1-V5
+++ b/dev/doc/README-V1-V5
@@ -1,10 +1,13 @@
 
                  Notes on the prehistory of Coq
 
-This archive contains the sources of the CONSTR ancestor of the Coq proof
-assistant. CONSTR, then Coq, was designed and implemented in the Formel team,
-joint between the INRIA Rocquencourt laboratory and the Ecole Normale Supérieure
-of Paris, from 1984 onwards.
+This document is a copy within the Coq archive of a document written
+in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin
+to accompany their public release of the archive of versions 1.10 to 6.2
+of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and
+implemented in the Formel team, joint between the INRIA Rocquencourt
+laboratory and the Ecole Normale Supérieure of Paris, from 1984
+onwards.
 
 Version 1
 
diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index a8b5d10da..70889badc 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -26,6 +26,6 @@ codesign -f -s - $APP
 
 # Create the dmg bundle
 mkdir -p $DMGDIR
-ln -s /Applications $DMGDIR
+ln -sf /Applications $DMGDIR/Applications
 cp -r $APP $DMGDIR
 hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
diff --git a/engine/evd.ml b/engine/evd.ml
index 60239ebfe..069fcbfa6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1096,9 +1096,12 @@ let meta_name evd mv =
 
 let clear_metas evd = {evd with metas = Metamap.empty}
 
-let meta_merge evd1 evd2 =
+let meta_merge ?(with_univs = true) evd1 evd2 =
   let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in
-  let universes = union_evar_universe_context evd2.universes evd1.universes in
+  let universes =
+    if with_univs then union_evar_universe_context evd2.universes evd1.universes
+    else evd2.universes
+  in
   {evd2 with universes; metas; }
 
 type metabinding = metavariable * constr * instance_status
diff --git a/engine/evd.mli b/engine/evd.mli
index 25d8a8c3d..57399f2b5 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -448,7 +448,7 @@ val meta_reassign  : metavariable -> constr * instance_status -> evar_map -> eva
 val clear_metas : evar_map -> evar_map
 
 (** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
-val meta_merge : evar_map -> evar_map -> evar_map
+val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map
 
 val undefined_metas : evar_map -> metavariable list
 val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d9aed87ed..21d1e7134 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -695,14 +695,13 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
   let indty, paramsletsubst =
-    let subst, inst = 
+    let _, _, subst, inst =
       List.fold_right
-	(fun (na, b, t) (subst, inst) ->
+	(fun (na, b, t) (i, j, subst, inst) ->
 	 match b with
-	 | None -> (mkRel 1 :: List.map (lift 1) subst,
-		   mkRel 1 :: List.map (lift 1) inst)
-	 | Some b -> (substl subst b) :: subst, List.map (lift 1) inst)
-	paramslet ([], [])
+	 | None -> (i-1, j-1, mkRel i :: subst, mkRel j :: inst)
+	 | Some b -> (i, j-1, substl subst b :: subst, inst))
+	paramslet (nparamargs, List.length paramslet, [], [])
     in
     let subst = (* For the record parameter: *)
       mkRel 1 :: List.map (lift 1) subst
@@ -732,14 +731,37 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
   in
   let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
     match b with
-    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst,
-		substl letsubst c :: subst)
+    | Some c ->
+        (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+        let c = liftn 1 j c in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c1 = substl subst c in
+        (* From [params, x:I |- subst:field1,..,fieldj]
+           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+           is represented with instance of field1 last *)
+        let subst = c1 :: subst in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c2 = substl letsubst c in
+        (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
+           to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
+        let letsubst = c2 :: letsubst in
+        (i, j+1, kns, pbs, subst, letsubst)
     | None ->
       match na with
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
-	let projty = substl letsubst (liftn 1 j t) in
-	let ty = substl subst (liftn 1 j t) in
+        (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+        let t = liftn 1 j t in
+        (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+	let projty = substl letsubst t in
+        (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+           to [params, x:I |- t(proj1 x,..,projj x)] *)
+	let ty = substl subst t in
 	let term = mkProj (Projection.make kn true, mkRel 1) in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 1b12cd42c..5d92fca5e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -681,7 +681,7 @@ and build_entry_lc_from_case env funname make_discr
 	let case_resl =
 	    List.fold_right
 	      (fun (case_arg,_) ctxt_argsl ->
-		let arg_res = build_entry_lc env funname avoid case_arg  in
+		let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in
 		combine_results combine_args arg_res ctxt_argsl
 	      )
 	      el
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 04936cd83..8cf365cea 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -212,9 +212,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pattern_of_constr (Global.env()) Evd.empty f, Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c
   in
   aux bodyi
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index fb629d049..83bf355cc 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -122,9 +122,6 @@ let head_of_constr_reference c = match kind_of_term c with
   | _ -> anomaly (Pp.str "Not a rigid reference")
 
 let pattern_of_constr env sigma t =
-  let ctx = ref [] in
-  let keep = ref Evar.Set.empty in
-  let remove = ref Evar.Set.empty in
   let rec pattern_of_constr env t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -143,14 +140,9 @@ let pattern_of_constr env sigma t =
     | App (f,a) ->
         (match
           match kind_of_term f with
-          | Evar (evk,args as ev) ->
+          | Evar (evk,args) ->
             (match snd (Evd.evar_source evk sigma) with
-              Evar_kinds.MatchingVar (true,id) ->
-		let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
-                  ctx := (id,None,ty)::!ctx;
-		  keep := Evar.Set.union (evars_of_term ty) !keep;
-		  remove := Evar.Set.add evk !remove;
-                  Some id
+              Evar_kinds.MatchingVar (true,id) -> Some id
             | _ -> None)
           | _ -> None
          with
@@ -162,13 +154,11 @@ let pattern_of_constr env sigma t =
     | Proj (p, c) -> 
       pattern_of_constr env (Retyping.expand_projection env sigma p c [])
     | Evar (evk,ctxt as ev) ->
-      remove := Evar.Set.add evk !remove;
       (match snd (Evd.evar_source evk sigma) with
       | Evar_kinds.MatchingVar (b,id) ->
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
-          ctx := (id,None,ty)::!ctx;
-	  let () = ignore (pattern_of_constr env ty) in
-          assert (not b); PMeta (Some id)
+	let () = ignore (pattern_of_constr env ty) in
+        assert (not b); PMeta (Some id)
       | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
@@ -189,12 +179,7 @@ let pattern_of_constr env sigma t =
 	       Array.to_list (Array.mapi branch_of_constr br))
     | Fix f -> PFix f
     | CoFix f -> PCoFix f in
-  let p = pattern_of_constr env t in
-  let remove = Evar.Set.diff !remove !keep in
-  let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in
-  (* side-effect *)
-  (* Warning: the order of dependencies in ctx is not ensured *)
-  (sigma,!ctx,p)
+  pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -234,7 +219,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  pi3 (pattern_of_constr env sigma c)
+	  pattern_of_constr env sigma c
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -259,7 +244,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pi3 (pattern_of_constr (Global.env()) Evd.empty t)
+	 pattern_of_constr (Global.env()) Evd.empty t
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 9e72280fe..014828028 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,8 +39,7 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> 
-  Evd.evar_map * named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index bc6e75c38..cb4b54ffc 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -373,12 +373,12 @@ let fchain_flags () =
   { (default_unify_flags ()) with
     allow_K_in_toplevel_higher_order_unification = true }
 
-let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv =
+let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
-      evd = meta_merge nextclenv.evd clenv.evd;
+      evd = meta_merge ?with_univs nextclenv.evd clenv.evd;
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index ca62c985e..5995d8700 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -50,7 +50,7 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
 (** {6 linking of clenvs } *)
 
 val clenv_fchain :
-  ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
+  ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
 (** {6 Unification with clenvs } *)
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0c8440fe5..2241fb821 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -175,6 +175,10 @@ and e_my_find_search db_list local_db hdc concl =
   in
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
+      let b = match Hints.repr_hint t with
+      | Unfold_nth _ -> 1
+      | _ -> b
+      in
       (b,
         let tac = function
         | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
@@ -254,8 +258,8 @@ module SearchProblem = struct
     let d = s'.depth - s.depth in
     let d' = Int.compare s.priority s'.priority in
     let nbgoals s = List.length (sig_it s.tacres) in
-    if not (Int.equal d' 0) then d'
-    else if not (Int.equal d 0) then d
+    if not (Int.equal d 0) then d
+    else if not (Int.equal d' 0) then d'
     else Int.compare (nbgoals s) (nbgoals s')
 
   let branching s =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7a8a3a97b..89d14fdc7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -918,7 +918,7 @@ let apply_on_clause (f,t) clause =
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
-  clenv_fchain argmv f_clause clause
+  clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5630d20b5..625088682 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -677,7 +677,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in
+	let pat = Patternops.pattern_of_constr env sigma cty in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -696,7 +696,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in
+	let pat = Patternops.pattern_of_constr env ce.evd c' in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -794,7 +794,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
+              pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
               code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 25d80b9c8..2597606aa 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -689,12 +689,12 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
       try Inl (coerce_to_evaluable_ref env x)
       with CannotCoerceTo _ ->
         let c = coerce_to_closed_constr env x in
-        Inr (pi3 (pattern_of_constr env sigma c)) in
+        Inr (pattern_of_constr env sigma c) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
      with Not_found ->
        error_global_not_found_loc loc (qualid_of_ident id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
-  | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
+  | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
 
 let interp_constr_with_occurrences_and_name_as_list =
@@ -1003,7 +1003,7 @@ let interp_induction_arg ist gl arg =
           try Sigma.here (constr_of_id env id', NoBindings) sigma
           with Not_found ->
             user_err_loc (loc, "interp_induction_arg",
-            pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.")
+            pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
           end })
       in
       try
@@ -1060,7 +1060,7 @@ let use_types = false
 let eval_pattern lfun ist env sigma ((glob,_),pat as c) =
   let bound_names = bound_glob_vars glob in
   if use_types then
-    (bound_names,pi3 (interp_typed_pattern ist env sigma c))
+    (bound_names,interp_typed_pattern ist env sigma c)
   else
     (bound_names,instantiate_pattern env sigma lfun pat)
 
@@ -2175,7 +2175,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Tacmach.New.project gl in
         Proofview.V82.tactic begin fun gl -> 
-          let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
+          let op = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
           let c_interp patvars = { Sigma.run = begin fun sigma ->
 	    let lfun' = Id.Map.fold (fun id c lfun ->
@@ -2191,7 +2191,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
           end } in
 	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
-	      { gl with sigma = sigma }
+	      gl
         end
       end }
       end
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f2e013641..e181c8e14 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -626,7 +626,7 @@ module New = struct
 	  errorlabstrm "Tacticals.general_elim_then_using"
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
-    let elimclause' = clenv_fchain indmv elimclause indclause in
+    let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
     let branchsigns = compute_construtor_signatures isrec ind in
     let brnames = compute_induction_names (Array.length branchsigns) allnames in
     let flags = Unification.elim_flags () in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c26ea5678..5cd17fad4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1347,7 +1347,9 @@ let simplest_elim c = default_elim false None (c,NoBindings)
 *)
 
 let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
-  try clenv_fchain ~flags mv elimclause hypclause
+  (** The evarmap of elimclause is assumed to be an extension of hypclause, so
+      we do not need to merge the universes coming from hypclause. *)
+  try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
   with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
     (* Set the hypothesis name in the message *)
     raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
@@ -1634,7 +1636,7 @@ 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.";
   let f mv =
-    try Some (find_matching_clause (clenv_fchain mv ~flags clause) innerclause)
+    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
@@ -3809,7 +3811,7 @@ let recolle_clenv i params args elimclause gl =
          trying to unify (which would lead to trying to apply it to
          evars if y is a product). *)
       let indclause  = mk_clenv_from_n gl (Some 0) (x,y) in
-      let elimclause' = clenv_fchain i acc indclause in
+      let elimclause' = clenv_fchain ~with_univs:false i acc indclause in
       elimclause')
     (List.rev clauses)
     elimclause
diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v
new file mode 100644
index 000000000..bf0e570ab
--- /dev/null
+++ b/test-suite/bugs/closed/4429.v
@@ -0,0 +1,31 @@
+Require Import Arith.Compare_dec.
+Require Import Unicode.Utf8.
+
+Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
+  match n with
+    | O    => x
+    | S n' => f (my_nat_iter n' f x)
+  end.
+
+Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
+  match mn with
+    | (0, 0)       => 0
+    | (0, S n')    => S n'
+    | (S m', 0)    => S m'
+    | (S m', S n') =>
+      match le_gt_dec (S m') (S n') with
+        | left  _ => f (S m', S n' - S m')
+        | right _ => f (S m' - S n', S n')
+      end
+  end.
+
+Axiom max_correct_l : ∀ m n : nat, m <= max m n.
+Axiom max_correct_r : ∀ m n : nat, n <= max m n.
+
+Hint Resolve max_correct_l max_correct_r : arith.
+
+Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
+Proof.
+  intros.
+  Timeout 3 eauto with arith.
+Qed.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 125615c53..281d707cb 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -194,4 +194,17 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
 Definition term (x : wrap nat) := x.(unwrap).
 Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
 Recursive Extraction term term'.
-(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file
+(*Unset Printing Primitive Projection Parameters.*)
+
+(* Primitive projections in the presence of let-ins (was not failing in beta3)*)
+
+Set Primitive Projections.
+Record s (x:nat) (y:=S x) := {c:=x; d:x=c}.
+Lemma f : 0=1.
+Proof.
+Fail apply d.
+(*
+split.
+reflexivity.
+Qed.
+*)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 0a10cfdc3..9cdb46064 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -289,7 +289,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	else if !refine_instance || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_program_mode () then
-	      let hook vis gr =
+	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
 		  Typeclasses.declare_instance pri (not global) (ConstRef cst)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3d338ee0a..0b709a3fc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -192,6 +192,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 	Obligations.eterm_obligations env ident evd 0 c typ
       in
       let ctx = Evd.evar_universe_context evd in
+      let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
@@ -1010,7 +1011,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let hook, recname, typ = 
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
-      let hook l gr = 
+      let hook l gr _ = 
 	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let pl, univs = Evd.universe_context !evdref in
@@ -1026,7 +1027,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	hook, name, typ
     else 
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook l gr = 
+      let hook l gr _ = 
 	if Impargs.is_implicit_args () || not (List.is_empty impls) then
 	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index de03e8356..b553700c4 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -318,7 +318,7 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : unit Lemmas.declaration_hook;
+  prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
   prg_opaque : bool;
 }
 
@@ -517,7 +517,7 @@ let declare_definition prg =
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r))
+      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
       
 open Pp
 
@@ -582,6 +582,7 @@ let declare_mutual_definition l =
   in
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
+  let fix_exn = Stm.get_fix_exn () in
   let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
@@ -589,8 +590,8 @@ let declare_mutual_definition l =
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr;
-      List.iter progmap_remove l; kn
+    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+    List.iter progmap_remove l; kn
 
 let shrink_body c = 
   let ctx, b = decompose_lam_assum c in
@@ -1020,7 +1021,7 @@ let show_term n =
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
 let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls =
+    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let info = str (Id.to_string n) ++ str " has type-checked" in
   let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
@@ -1038,7 +1039,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind =
+    ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 61a8ee520..2e3aa6005 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -68,7 +68,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -84,7 +84,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool ->
+  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit