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

1 files changed, 2 insertions, 0 deletions

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 *)