From bfce815bd1fa2c603141661b209a864c67ae1dbf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 16 Mar 2016 18:00:25 +0100
Subject: Fix incorrect behavior of CS resolution

Due to a change in pretyping, using cast annotations as typing
constraints, the canonical structure problems given to the unification
could contain non-evar-normalized terms, hence we force
evar normalization where necessary to ensure the same CS solutions
can be found. Here the dependency test is fooled by an erasable
dependency, and the following resolution needs a independent codomain
for pop b to be well-scoped.
---
 pretyping/evarconv.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 690b974be5..b8d92b9be7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -138,6 +138,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
     try
       match kind_of_term t2 with
 	Prod (_,a,b) -> (* assert (l2=[]); *)
+	  let _, a, b = destProd (Evarutil.nf_evar sigma t2) in
       	  if dependent (mkRel 1) b then raise Not_found
 	  else lookup_canonical_conversion (proji, Prod_cs),
 	    (Stack.append_app [|a;pop b|] Stack.empty)
-- 
cgit v1.2.3


From 82b371aceb1ef6b1e15bdace2cf142e65724a3c6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 17 Mar 2016 17:53:25 +0100
Subject: Fix #4623: set tactic too weak with universes (regression)

The regression was introduced by efa1c32a4d178, which replaced
unification by conversion when looking for more occurrences of a
subterm. The conversion function called was not the right one, as it
was not inferring constraints.
---
 pretyping/unification.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9b6e856b80..cd0bbfa300 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1532,8 +1532,9 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     | e when Errors.noncritical e -> raise (NotUnifiable None) in
   let merge_fun c1 c2 =
     match c1, c2 with
-    | Some (evd,c1,_) as x, Some (_,c2,_) ->
-      if is_conv env sigma c1 c2 then x else raise (NotUnifiable None)
+    | Some (evd,c1,x), Some (_,c2,_) ->
+      let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
+      if b then Some (evd, c1, x) else raise (NotUnifiable None)
     | Some _, None -> c1
     | None, Some _ -> c2
     | None, None -> None in
-- 
cgit v1.2.3