From 46a866aa5fd63cc577c4a453bcf26ee75c47c433 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 25 Jul 2016 15:00:47 +0200
Subject: Fix bug #4754, allow conversion problems to remain

when checking that the rewrite relation is homogeneous in
setoid_rewrite.
---
 tactics/rewrite.ml | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c7cfc4dc72..0892dc9e6c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -424,14 +424,22 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
+let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
+  pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
+
+let problem_inclusion x y =
+  List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
+               
 let evd_convertible env evd x y =
   try
-    let evd = Evarconv.the_conv_x env x y evd in
     (* Unfortunately, the_conv_x might say they are unifiable even if some
-        unsolvable constraints remain, so we check them here *)
-    let evd = Evarconv.consider_remaining_unif_problems env evd in
-    let () = Evarconv.check_problems_are_solved env evd in
-    Some evd
+       unsolvable constraints remain, so we check that this unification 
+       does not introduce any new problem. *)
+    let _, pbs = Evd.extract_all_conv_pbs evd in
+    let evd' = Evarconv.the_conv_x env x y evd in
+    let _, pbs' = Evd.extract_all_conv_pbs evd' in
+    if evd' == evd || problem_inclusion pbs' pbs then Some evd'
+    else None
   with e when Errors.noncritical e -> None
 
 let convertible env evd x y =
-- 
cgit v1.2.3


From 25ef9dda0311213bb2f6e2b9cd0b87be2128599b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 25 Jul 2016 15:44:53 +0200
Subject: Fix #4769, univ poly and elim schemes in sections

---
 tactics/elimschemes.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 4ff774b8e5..ba23568af1 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -51,19 +51,21 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let u = Univ.UContext.instance ctx in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
-    let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
+    let sigma = Evd.merge_universe_context sigma ectx in
+    let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
       (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
+  let sigma = Evd.from_env env in
   let ctx = 
     let mib,mip = Inductive.lookup_mind_specif env ind in
       Declareops.inductive_context mib
   in
   let u = Univ.UContext.instance ctx in
   let ctxset = Univ.ContextSet.of_context ctx in
-  let ectx = Evd.evar_universe_context_of ctxset in
-  let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
+  let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in
+  let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
     c, Evd.evar_universe_context sigma
  
 let rect_scheme_kind_from_type =
-- 
cgit v1.2.3