Prise en compte d'un inductif sans argument dans le 'in' des 'match'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4498 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 11 insertions, 8 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f8bd7b3d9b..701e14e173 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -661,6 +661,7 @@ let internalise sigma env allow_soapp lvar c =
 	let tids = List.fold_right Idset.add tids Idset.empty in
 	let t = intern_type (tids,[],None,scopes) t in
 	begin match t with
+	  | RRef (loc,IndRef ind) -> ids,Some (loc,ind,[])
 	  | RApp (loc,RRef (_,IndRef ind),l) ->
 	      let nal = List.map (function
 		| RHole _ -> Anonymous
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f83c6e3508..1a9a66270b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -536,14 +536,16 @@ let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
 
 (* Used in correctness and interface *)
 
-let names_of_cases_indtype =
-  let rec aux ids = function
-    (* We deal only with the regular cases *)
-  | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> aux ids a) ids l
-  | CNotation (_,_,l) | CAppExpl (_,_,l) -> List.fold_left aux ids l
-  | CRef (Ident (_,id)) -> id::ids
-  | _ -> ids
-  in aux []
+
+let names_of_cases_indtype t =
+  let push_ref ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
+  match t with
+  (* We deal only with the regular cases *)
+  | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> push_ref ids a) [] l
+  | CNotation (_,_,l)
+    (* assume the ntn is applicative and does not instantiate the head !! *)
+  | CAppExpl (_,_,l) -> List.fold_left push_ref [] l
+  | _ -> []
 
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e