From 487042107e8d7f3fd0350ade726e11d9ba4b6214 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Oct 2000 20:10:10 +0000
Subject: Renommage des find_m*type

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

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 655a4903e8..9d536b644a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -283,7 +283,6 @@ let substnl_tomatch v depth = function
 
 let subst_tomatch (depth,c) = substnl_tomatch [c] depth
 
-
 (**********************************************************************)
 (* Dealing with regular and default patterns *)
 let is_regular eqn = eqn.tag = RegularPat
@@ -762,12 +761,16 @@ let build_branch pb defaults eqns const_info =
   let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
   if submat = [] & submatdef = [] then error "Non exhaustive";
   let typs = List.map2 (fun (_,t) na -> (na,t)) cs_args (List.rev names) in
+  let _,typs' =
+    List.fold_right
+      (fun (na,t) (env,typs) ->
+ 	 (push_rel_decl (na,outcast_type t) env,
+	  ((na,to_mutind env !(pb.isevars) t),t)::typs))
+      typs (pb.env,[]) in
   let tomatchs =
     List.fold_left2
-      (fun l (na,t) dep_in_rhs ->
-	 ((na,to_mutind pb.env !(pb.isevars) t),
-	  (find_dependencies t l dep_in_rhs))::l)
-      [] typs (dependencies_in_rhs const_info.cs_nargs eqns) in
+      (fun l (d,t) dep_in_rhs -> (d,find_dependencies t l dep_in_rhs)::l)
+      [] typs' (dependencies_in_rhs const_info.cs_nargs eqns) in
   let topushs = List.map (fun x -> ToPush x) tomatchs in
   (* The dependent term to subst in the types of the remaining UnPushed 
      terms is relative to the current context enriched by topushs *)
-- 
cgit v1.2.3