X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fregtest.ml;h=bee1c28166a54f555ee0448253b4f32b08a6b774;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=7836fae472848fa423dd923e2437f7ab8f96aac6;hpb=8eb9b5bc9507708e51c1d2d8616bb7b963aa6ff5;p=helm.git diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 7836fae47..bee1c2816 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -227,11 +227,13 @@ let as_expected report_fname expected found = let test_this mqi_handle uri_pred raw_term = let empty_context = [] in List.map - (function (env, metasenv, cic_term) -> + (function (env, metasenv, cic_term,ugraph ) -> let etype = try - CicPp.ppterm - (CicTypeChecker.type_of_aux' metasenv empty_context cic_term) + let ty, _ = + (CicTypeChecker.type_of_aux' metasenv empty_context cic_term ugraph) + in + CicPp.ppterm ty with _ -> "MALFORMED" in let ereduced = @@ -246,7 +248,7 @@ let test_this mqi_handle uri_pred raw_term = etype = etype ^ "\n"; ereduced = ereduced ^ "\n"; } - ) (BatchParser.parse mqi_handle ~uri_pred raw_term) + ) (BatchParser.parse mqi_handle ~uri_pred raw_term CicUniv.empty_ugraph) let dump_environment filename = try