*)
C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
| C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
- | C.Prod (C.Anonymous,source,dest) ->
- strictly_positive context n nn
- (subst_inductive_type_with_dummy_mutind source) &&
- weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
| C.Prod (name,source,dest) when
- does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+ does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
(* dummy abstraction, so we behave as in the anonimous case *)
strictly_positive context n nn
(subst_inductive_type_with_dummy_mutind source) &&
raise (TypeCheckerFailure
(lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
UriManager.string_of_uri uri)))
- | C.Prod (C.Anonymous,source,dest) ->
- let b = strictly_positive context n nn source in
- b &&
- are_all_occurrences_positive
- ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
- (i+1) (n + 1) (nn + 1) dest
| C.Prod (name,source,dest) when
- does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+ does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
(* dummy abstraction, so we behave as in the anonimous case *)
strictly_positive context n nn source &&
are_all_occurrences_positive
| C.LetIn (n,s,ty,t) ->
(* only to check if s is well-typed *)
let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+ let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
let b,ugraph1 =
R.are_convertible ~subst ~metasenv context ty ty' ugraph1
in
let (_,ty,_) = List.nth fl i in
ty,ugraph2
- and check_exp_named_subst ~logger ~subst context ugraph =
+ and check_exp_named_subst ~logger ~subst context =
let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
match l with
[] -> ugraph
raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
end
in
- check_exp_named_subst_aux ~logger [] ugraph
+ check_exp_named_subst_aux ~logger []
and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
let module C = Cic in