From ff2da62916d9a6bec4aae1a576ce5d396ea9893e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 Jun 2014 17:27:24 +0200
Subject: Fix program cases and inversion tactic to correctly record universe
 constraints. Fixes FingerTree contrib.

---
 pretyping/cases.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b5aeeae3ab..50396d8547 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2155,6 +2155,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
+	 let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
-- 
cgit v1.2.3