From b13a0995c13c51dd997182997762fe8798ee4a5b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Nov 2002 18:06:57 +0000 Subject: [PATCH] Metasenv partially checked. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) 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 *) -- 2.39.2