X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=11d68b78c052d0d653bb2b73372c3afd160d2dee;hb=0373aa12449568c5aca2027d8e8773ea0c0fa4a5;hp=b539508a1212f10672a08f46691e486be41ba97e;hpb=c929e791b0eca1e75694a663a2f6ada9f0ff9534;p=helm.git

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 =