From 5efbe2d6be224aea70bf570b7ee26d80d79bc54f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 1 Oct 2000 15:12:51 +0000
Subject: Renommage AppL en App; Suppression cast

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

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ac778ded80..3b3c09d384 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -21,8 +21,7 @@ open Evarconv
 (* A) Typing old cases                                               *)
 (* This was previously in Indrec but creates existential holes       *)
 
-let mkExistential isevars env =
-  new_isevar isevars env (mkCast (dummy_sort, dummy_sort)) CCI
+let mkExistential isevars env = new_isevar isevars env dummy_sort CCI
 
 let norec_branch_scheme env isevars cstr =
   it_mkProd_or_LetIn (mkExistential isevars env) cstr.cs_args 
-- 
cgit v1.2.3