Metasenv partially checked.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 7e96de2a42aca82b8acdc7e7d57ebba1d949840a..a494c4a690f519638efacbe63738446e9f100245 100644 (file)
--- 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 *)