From 07f0871dde38d6e5bfa57a36071e72ca7c207a39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 9 Nov 2014 19:59:13 +0100
Subject: Fixing bug #3792.

Pretyping of [if] cases was missing a convertibility check with the ambient
type constraint, and just dropped it. This was making the pretyper construct
ill-typed terms.
---
 pretyping/pretyping.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 16d92ad78..71ed28c97 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -847,7 +847,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	  Typing.check_allowed_sort env !evdref ind cj.uj_val pred;
 	  mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
-	{ uj_val = v; uj_type = p }
+      let cj = { uj_val = v; uj_type = p } in
+      inh_conv_coerce_to_tycon loc env evdref cj tycon
 
   | GCases (loc,sty,po,tml,eqns) ->
     Cases.compile_cases loc sty
-- 
cgit v1.2.3