From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Jun 2002 10:45:28 +0000 (+0000)
Subject: *** empty log message ***
X-Git-Tag: V_0_3_0_debian_8~29
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=951c33fd9cc306f3c214fb74cddf509839ca7a14;p=helm.git

*** empty log message ***
---

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 =