From 449e8a54371b0c707bb7e3c5acdb4fd475a016d0 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 3 May 2018 11:03:27 +0100
Subject: Work in progress on the coq backend - originally based on the Lem
 backend - added externs to some of the library files and tests - added
 wildcard to extern valspecs in parser - added Type_check.get_val_spec_orig to
 return the valspec with the   function's original names for bound type
 variables

Note that most of the tests will fail currently
---
 src/process_file.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/process_file.mli')

diff --git a/src/process_file.mli b/src/process_file.mli
index 2f418ff9..b38b4259 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -56,6 +56,7 @@ val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Typ
 val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_coq : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_c : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
@@ -81,6 +82,7 @@ val opt_dall_split_errors : bool ref
 type out_type =
   | Lem_ast_out
   | Lem_out of string list (* If present, the strings are files to open in the lem backend*)
+  | Coq_out of string list (* If present, the strings are files to open in the coq backend*)
 
 val output :
   string ->                           (* The path to the library *)
-- 
cgit v1.2.3