- List.iter2
- (fun t ct ->
- let res =
- match (t,ct) with
- _,None -> true
- | Some t,Some (_,C.Def ct) ->
- R.are_convertible context t ct
- | Some t,Some (_,C.Decl ct) ->
- R.are_convertible context (type_of_aux' metasenv context t) ct
- | _, _ -> false
- in
- if not res then raise MetasenvInconsistency
- ) l lifted_canonical_context
+ List.iter2
+ (fun t ct ->
+ let res =
+ match (t,ct) with
+ _,None -> true
+ | Some t,Some (_,C.Def ct) ->
+ R.are_convertible context t ct
+ | Some t,Some (_,C.Decl ct) ->
+ R.are_convertible context (type_of_aux' metasenv context t) ct
+ | _, _ -> false
+ in
+ if not res then raise MetasenvInconsistency
+ ) l lifted_canonical_context