From 066998ff9f89404cb41a6a3f8c0ccc88d2cc7a4b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 27 Dec 2003 20:12:01 +0000
Subject: Type le 'return' comme un type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c240613ae5..25b41d069c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1675,7 +1675,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       (* We extract the signature of the arity *)
       let arsign = extract_arity_signature env tomatchs sign in
       let env = push_rels arsign env in
-      let predccl = (typing_fun empty_tycon env rtntyp).uj_val in
+      let predccl = (typing_fun (mk_tycon (new_Type ())) env rtntyp).uj_val in
       Some
         (build_initial_predicate env (evars_of isevars) true predccl tomatchs)
 
-- 
cgit v1.2.3