From 2ab4324677baa86bfd15716cae965f066bad7e53 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Jan 2006 18:28:07 +0000
Subject: Bug 'match x in I' (potentiellement utilisable comme cast)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7946 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/topconstr.ml | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 60e117d9ea..6a4ad1f59b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -653,17 +653,16 @@ let coerce_to_id = function
 
 
 let names_of_cases_indtype =
-  let rec vars_of ids t =
-    match t with
-      (* We deal only with the regular cases *)
-      | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> vars_of ids a) [] l
-      | CRef (Ident (_,id)) -> id::ids
-      | CNotation (_,_,l)
-      (* assume the ntn is applicative and does not instantiate the head !! *)
-      | CAppExpl (_,_,l) -> List.fold_left vars_of [] l
-      | CDelimiters(_,_,c) -> vars_of ids c
-      | _ -> ids in
-  vars_of []
+  let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
+  let rec vars_of = function
+    (* We deal only with the regular cases *)
+    | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
+    | CNotation (_,_,l)
+    (* assume the ntn is applicative and does not instantiate the head !! *)
+    | CAppExpl (_,_,l) -> List.fold_left add_var [] l
+    | CDelimiters(_,_,c) -> vars_of c
+    | _ -> [] in
+  vars_of
 
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
-- 
cgit v1.2.3