From ccdc62a6b4722c38f2b37cbf21b14e5094255390 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 21 Jan 2016 18:05:55 -0500
Subject: Fix bug #4506. Using betadeltaiota_nolet might produce terms of the
 form (let x := t in u) a that should be reduced. Maybe a different
 decomposition/reduction primitive should be used instead.

---
 pretyping/indrec.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index d5f6e9b301..0588dcc87f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -155,7 +155,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	| Prod (n,t,c) ->
 	    let d = (n,None,t) in
 	    make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
-	| LetIn (n,b,t,c) ->
+	| LetIn (n,b,t,c) when List.is_empty largs ->
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
      	| Ind (_,_) ->
@@ -166,7 +166,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
                 base [|applist (mkRel (i+1), Termops.extended_rel_list 0 sign)|]
             else
 	      base
-      	| _ -> assert false
+      	| _ ->
+	   let t' = whd_betadeltaiota env sigma p in
+	   if Term.eq_constr p' t' then assert false
+	   else prec env i sign t'
     in
     prec env 0 []
   in
@@ -230,14 +233,17 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	| Prod (n,t,c) ->
 	    let d = (n,None,t) in
 	    mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
-	| LetIn (n,b,t,c) ->
+	| LetIn (n,b,t,c) when List.is_empty largs ->
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
             let realargs = List.skipn nparrec largs
             and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
-     	| _ -> assert false
+     	| _ ->
+	   let t' = whd_betadeltaiota env sigma p in
+	     if Term.eq_constr t' p' then assert false
+	     else prec env i hyps t'
     in
     prec env 0 []
   in
-- 
cgit v1.2.3


From 6a046f8d3e33701d70e2a391741e65564cc0554d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 23 Jan 2016 15:55:43 -0500
Subject: Fix bug #4519: oops, global shadowed local universe level bindings.

---
 pretyping/pretyping.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ac0104d9f8..b33084a423 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -138,12 +138,12 @@ let interp_universe_level_name evd (loc,s) =
 	 in evd, level
     else 
       try
-	let id =
-	  try Id.of_string s with _ -> raise Not_found in
-	  evd, Idmap.find id names
+	let level = Evd.universe_of_name evd s in
+	evd, level
       with Not_found ->
-	try let level = Evd.universe_of_name evd s in
-	      evd, level
+	try 
+	  let id = try Id.of_string s with _ -> raise Not_found in
+	  evd, Idmap.find id names
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
   	    new_univ_level_variable ~name:s univ_rigid evd
-- 
cgit v1.2.3


From 22a2cc1897f0d9f568ebfb807673e84f6ada491a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 27 Jan 2016 09:36:47 +0100
Subject: Fix bug #4537: Coq 8.5 is slower in typeclass resolution.

The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
---
 pretyping/evd.ml  | 4 ++++
 pretyping/evd.mli | 1 +
 2 files changed, 5 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 01083142b7..5441145189 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1467,6 +1467,10 @@ let map_metas_fvalue f evd =
   in
   set_metas evd (Metamap.smartmap map evd.metas)
 
+let map_metas f evd =
+  let map cl = map_clb f cl in
+  set_metas evd (Metamap.smartmap map evd.metas)
+
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
     | Clval(_,b,_) -> Some b
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 0b4f185368..9cfca02ed8 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -455,6 +455,7 @@ 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
+val map_metas : (constr -> constr) -> evar_map -> evar_map
 
 type metabinding = metavariable * constr * instance_status
 
-- 
cgit v1.2.3