From 9f0c1b70b2cc44c17d14ec085d44e1640edf021b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 25 Apr 2006 12:29:07 +0000
Subject: Code mort (suite)

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

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 71944b5639..57946eacc7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1634,9 +1634,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
   let tmsign = List.map snd tomatchl in
   let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
     
-  (* We deal with initial aliases *)
-  let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
-    
   (* We push the initial terms to match and push their alias to rhs' envs *)
   (* names of aliases will be recovered from patterns (hence Anonymous here) *)
   let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-- 
cgit v1.2.3