From c907f31fd8f4b12bf2d7df2078603dbe804475a2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 4 Sep 2014 00:40:12 +0200
Subject: Add test-suite file for Case derivation on primitive records.

---
 pretyping/indrec.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 547268ef08..54f76fa33f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -105,8 +105,10 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 			  Termops.rel_vect ndepar k)
 	| Some ps -> 
 	  let term = mkApp (mkRel 2, Array.map (fun p -> mkProj (p, mkRel 1)) ps) in
-	  let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
-	    mkCast (term, DEFAULTcast, ty)
+	    if dep then
+	      let ty = mkApp (mkRel 3, [| mkRel 1 |]) in 
+		mkCast (term, DEFAULTcast, ty)
+	    else term
       in
 	it_mkLambda_or_LetIn_name env' obj deparsign
     else
-- 
cgit v1.2.3