let module U = UriManager in
function
C.Rel m when m > n && m <= nn -> false
- | C.Rel n ->
+ | C.Rel m ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> true
| Some (_,C.Def (bo,_)) ->
- guarded_by_destructors context n nn kl x safes bo
+ guarded_by_destructors context m nn kl x safes
+ (CicSubstitution.lift m bo)
| None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
)
| C.Meta _
| Cic.Variable (_,None,_,_) -> ()
| _ ->
raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
+ ("Unknown variable definition:" ^
UriManager.string_of_uri uri))
) ;
let typeoft = type_of_aux context t in
| (hete, hety)::tl ->
(match (CicReduction.whd context hetype) with
Cic.Prod (n,s,t) ->
- if CicReduction.are_convertible context s hety then
+ if CicReduction.are_convertible context hety s then
(CicReduction.fdebug := -1 ;
eat_prods context (CicSubstitution.subst hete t) tl
)