diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 4284a252..8c996c14 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -44,7 +44,7 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -(* XXX: for debugging the developing code: open Coq_ast *) +open Type_internal (* let r = Ulib.Text.of_latin1 *) @@ -69,6 +69,9 @@ let parse_file (f : string) : Parse_ast.defs = | Lexer.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) +let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs = + Initial_check.to_ast Nameset.empty Kindmap.empty Typmap.empty [] defs + (* type instances = Types.instance list Types.Pfmap.t let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list) |