| 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
)