*** empty log message ***

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index b539508a1212f10672a08f46691e486be41ba97e..11d68b78c052d0d653bb2b73372c3afd160d2dee 100644 (file)
--- 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 =