-let rec recursive uri typeno subst = function
- | Cic.Prod (_, _, target) -> recursive uri typeno subst target
- | Cic.MutInd (uri', typeno', subst')
- | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: _) ->
- UriManager.eq uri uri' && typeno = typeno' && subst = subst'
-(* | Cic.Appl args -> List.exists (recursive uri typeno subst) args *)
+let rec recursive uri typeno = function
+ | Cic.Prod (_, _, target) -> recursive uri typeno target
+ | Cic.MutInd (uri', typeno', [])
+ | Cic.Appl (Cic.MutInd (uri', typeno', []) :: _) ->
+ UriManager.eq uri uri' && typeno = typeno'