From 8e482fc932fa2b1893025d914d42dd17881c2fac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2015 18:51:33 +0100
Subject: Being more precise and faithful about the origin of the file
 reporting about the prehistory of Coq.

---
 dev/doc/README-V1-V5 | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5
index 2ca62e3d74..ebbc057734 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
 
-- 
cgit v1.2.3


From af399d81b0505d1f0be8e73cf45044266d5749e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Nov 2015 12:39:35 +0100
Subject: Performance fix for destruct.

The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
---
 pretyping/evd.ml   | 7 +++++--
 pretyping/evd.mli  | 2 +-
 proofs/clenv.ml    | 4 ++--
 proofs/clenv.mli   | 2 +-
 tactics/tactics.ml | 4 +++-
 5 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4a9466f4f3..c9b9f34414 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1550,9 +1550,12 @@ let meta_with_name evd id =
 
 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/pretyping/evd.mli b/pretyping/evd.mli
index 5c508419a4..117e52958b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -451,7 +451,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/proofs/clenv.ml b/proofs/clenv.ml
index a2cccc0e0b..5de8338ab6 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -379,12 +379,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 eb10817069..26e803354e 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -51,7 +51,7 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
 
 val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 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/tactics.ml b/tactics/tactics.ml
index 0a013e95f7..0551787e3a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1319,7 +1319,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)))
-- 
cgit v1.2.3


From c4fef5b9d2be739cad030131fd6fc4c07d5e2e08 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Nov 2015 19:24:41 +0100
Subject: More optimizations of [Clenv.clenv_fchain].

Everywhere we know that the universes of the left argument are an
extension of the right argument, we do not have to merge universes.
---
 tactics/equality.ml  | 2 +-
 tactics/tacticals.ml | 2 +-
 tactics/tactics.ml   | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 674c85af79..fe0ca61c66 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -914,7 +914,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/tacticals.ml b/tactics/tacticals.ml
index bc82e9ef46..4cce891a2a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -620,7 +620,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 0551787e3a..8daa7c4b86 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1605,7 +1605,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
@@ -3756,7 +3756,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
-- 
cgit v1.2.3


From c71aa6bd368b801bb17d4da69d1ab1e2bd7cbf39 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 7 Nov 2015 07:20:34 +0100
Subject: Fixing logical bugs in the presence of let-ins in computiong
 primitive projections.

- lift accounting for the record missing in computing the subst from
  fields to projections of the record
- substitution for parameters should not lift the local definitions
- typo in building the latter (subst -> letsubst)
---
 kernel/indtypes.ml                 | 17 +++++++++--------
 test-suite/success/primitiveproj.v | 15 ++++++++++++++-
 2 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 351de9ee88..f08f0b7bbb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -654,13 +654,12 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
       matching with a parameter context. *)
   let indty, paramsletsubst =
     let subst, inst = 
-      List.fold_right
-	(fun (na, b, t) (subst, inst) ->
+      List.fold_right_i
+	(fun i (na, b, t) (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 -> (mkRel i :: subst, mkRel i :: inst)
+	 | Some b -> (substl subst b) :: subst, inst)
+	1 paramslet ([], [])
     in
     let subst = (* For the record parameter: *)
       mkRel 1 :: List.map (lift 1) subst
@@ -690,8 +689,10 @@ 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 ->
+        let c = liftn 1 j c in
+        (i, j+1, kns, pbs, substl subst c :: subst,
+         substl letsubst c :: letsubst)
     | None ->
       match na with
       | Name id ->
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 125615c535..281d707cb3 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.
+*)
-- 
cgit v1.2.3


From df04191b48350b76a7650cccc68c9dfc60447787 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 7 Nov 2015 07:33:55 +0100
Subject: Slightly documenting code for building primitive projections.

---
 kernel/indtypes.ml | 29 +++++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f08f0b7bbb..6c32626ad9 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -690,15 +690,36 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
   let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
     match b with
     | 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
-        (i, j+1, kns, pbs, substl subst c :: subst,
-         substl letsubst c :: letsubst)
+        (* 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
-- 
cgit v1.2.3


From 23e6963a8168756f225ea2ae75fcf2af6952c6c3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 18 Nov 2015 14:50:35 +0100
Subject: MacOS package script: do not fail if link to /Applications already
 exists.

---
 dev/make-macos-dmg.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index a8b5d10dad..70889badc1 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
-- 
cgit v1.2.3


From 6f88442be8275361a7b68fd56d40976fdee9f4d5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 18 Nov 2015 15:58:17 +0100
Subject: Improve error message.

---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 355745d970..d244129425 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -989,7 +989,7 @@ let interp_induction_arg ist gl arg =
           try sigma, (constr_of_id env id', NoBindings)
           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."))
       in
       try
         (** FIXME: should be moved to taccoerce *)
-- 
cgit v1.2.3


From 0346ee4472711fc30b7cf197c1bad5c32140f831 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 18 Nov 2015 17:10:44 +0100
Subject: Fix a bug preventing the generation of graphs when doing multiple
 pattern-matching on function calls.

---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 1b12cd42ce..5d92fca5ea 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
-- 
cgit v1.2.3


From 6ababf42b3f03926c30cfbd209436ec83a21769e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 18 Nov 2015 17:04:12 +0100
Subject: Fixing fix c71aa6b to primitive projections.

- Introduced an error: fold was counting in the wrong direction and I
  did not test it. Sorry.
- Substitution from params-with-let to params-without-let was still
  not correct.

Hopefully everything ok now. Eventually, we should use canonical
combinators for that: extended_rel_context to built the instance and
and a combinator apparently yet to define for building a substitution
contracting the let-ins.
---
 kernel/indtypes.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6c32626ad9..a46c33bf03 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -653,13 +653,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 = 
-      List.fold_right_i
-	(fun i (na, b, t) (subst, inst) ->
+    let _, _, subst, inst =
+      List.fold_right
+	(fun (na, b, t) (i, j, subst, inst) ->
 	 match b with
-	 | None -> (mkRel i :: subst, mkRel i :: inst)
-	 | Some b -> (substl subst b) :: subst, inst)
-	1 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
-- 
cgit v1.2.3


From 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 19 Nov 2015 17:48:32 +0100
Subject: Fix bug #4433, removing hack on evars appearing in a pattern from a
 constr, and the associated signature, not needed anymore. Update CHANGES, no
 evar_map is produced by pattern_of_constr anymore.

---
 CHANGES                  |  2 --
 plugins/quote/quote.ml   |  4 ++--
 pretyping/patternops.ml  | 29 +++++++----------------------
 pretyping/patternops.mli |  3 +--
 tactics/hints.ml         |  6 +++---
 tactics/tacinterp.ml     | 10 +++++-----
 6 files changed, 18 insertions(+), 36 deletions(-)

diff --git a/CHANGES b/CHANGES
index 719be44929..07d6281717 100644
--- a/CHANGES
+++ b/CHANGES
@@ -107,8 +107,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/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2a2ef30fb1..b72ebbc927 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,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 fb629d049f..83bf355cc2 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 9e72280fe2..0148280287 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/tactics/hints.ml b/tactics/hints.ml
index 5630d20b5d..6250886821 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 d244129425..ee21a51598 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -688,12 +688,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 =
@@ -1043,7 +1043,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)
 
@@ -2154,7 +2154,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma 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 =
 	    let lfun' = Id.Map.fold (fun id c lfun ->
@@ -2167,7 +2167,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.")
           in
 	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
-	      { gl with sigma = sigma }
+	      gl
         end
       end
       end
-- 
cgit v1.2.3


From cfc0fc0075784e75783c9b4482fd3f4b858a44bf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 19 Nov 2015 17:49:32 +0100
Subject: Allow program hooks to see the refined universe_context at the end of
 a definition, if they manipulate structures depending on the initial state of
 the context.

---
 toplevel/classes.ml      |  2 +-
 toplevel/command.ml      |  5 +++--
 toplevel/obligations.ml  | 13 +++++++------
 toplevel/obligations.mli |  4 ++--
 4 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c354c7d32f..6de0a9f55c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -288,7 +288,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 3d338ee0a3..0b709a3fc4 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 9019f486be..311c61f894 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 c in
@@ -987,7 +988,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
@@ -1005,7 +1006,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 61a8ee520f..2e3aa60054 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
 
-- 
cgit v1.2.3


From 574e510ba069f1747ecb1e5a17cf86c902d79d44 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Nov 2015 18:40:32 +0100
Subject: Fix bug #4429: eauto with arith: 70x performance regression in Coq
 8.5.

The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.

Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.
---
 tactics/eauto.ml4             |  8 ++++++--
 test-suite/bugs/closed/4429.v | 31 +++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4429.v

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ee7b94b0d1..20a7448dcb 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -166,6 +166,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)
@@ -245,8 +249,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/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v
new file mode 100644
index 0000000000..bf0e570ab8
--- /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.
-- 
cgit v1.2.3