From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Nov 2002 18:06:57 +0000 (+0000)
Subject: Metasenv partially checked.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b13a0995c13c51dd997182997762fe8798ee4a5b;p=helm.git

Metasenv partially checked.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 7e96de2a4..a494c4a69 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1644,10 +1644,16 @@ let typecheck uri =
           (* only to check that ty is well-typed *)
           let _ = type_of ty in ()
         | C.CurrentProof (_,conjs,te,ty,_) ->
-            (*CSC: bisogna controllare anche il metasenv!!! *)
+           let _ =
+            List.fold_left
+             (fun metasenv ((_,context,ty) as conj) ->
+               ignore (type_of_aux' metasenv context ty) ;
+               metasenv @ [conj]
+             ) [] conjs
+           in
             let _ = type_of_aux' conjs [] ty in
-             debug (type_of_aux' conjs [] te) [] ;
-             if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then
+             if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
+             then
               raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
         | C.Variable (_,bo,ty,_) ->
            (* only to check that ty is well-typed *)