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(+)

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