From 951c33fd9cc306f3c214fb74cddf509839ca7a14 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Jun 2002 10:45:28 +0000 Subject: [PATCH] *** empty log message *** --- .../cic_proof_checking/cicTypeChecker.ml | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index b539508a1..11d68b78c 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1134,19 +1134,19 @@ and check_metasenv_consistency metasenv context canonical_context l = in aux 1 canonical_context in - 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 (* type_of_aux' is just another name (with a different scope) for type_of_aux *) and type_of_aux' metasenv context t = -- 2.39.2