1 files changed, 77 insertions, 0 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
new file mode 100644
index 00000000..ad1c4391
--- /dev/null
+++ b/interp/constrextern.mli
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: constrextern.mli,v 1.11.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+
+(*i*)
+open Util
+open Names
+open Term
+open Termops
+open Sign
+open Environ
+open Libnames
+open Nametab
+open Rawterm
+open Pattern
+open Topconstr
+open Symbols
+(*i*)
+
+(* v7->v8 translation *)
+val id_of_v7_string : string -> identifier
+val v7_to_v8_id : identifier -> identifier (* v7->v8 translation *)
+val shortest_qualid_of_v7_global : Idset.t -> global_reference -> qualid
+val check_same_type : constr_expr -> constr_expr -> unit
+
+(* Translation of pattern, cases pattern, rawterm and term into syntax
+   trees for printing *)
+
+val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
+val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
+val extern_rawtype : Idset.t -> rawconstr -> constr_expr
+val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
+
+(* If [b=true] in [extern_constr b env c] then the variables in the first 
+   level of quantification clashing with the variables in [env] are renamed *)
+
+val extern_constr : bool -> env -> constr -> constr_expr
+val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
+val extern_reference : loc -> Idset.t -> global_reference -> reference
+
+(* Printing options *)
+val print_implicits : bool ref
+val print_arguments : bool ref
+val print_evar_arguments : bool ref
+val print_coercions : bool ref
+val print_universes : bool ref
+val print_no_symbol : bool ref
+val print_projections : bool ref
+
+(* This governs printing of implicit arguments. If [with_implicits] is
+   on and not [with_arguments] then implicit args are printed prefixed
+   by "!"; if [with_implicits] and [with_arguments] are both on the
+   function and not the arguments is prefixed by "!" *)
+val with_implicits : ('a -> 'b) -> 'a -> 'b
+val with_arguments : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing of coercions *)
+val with_coercions : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing universe names of Type{.} *)
+val with_universes : ('a -> 'b) -> 'a -> 'b
+
+(* This suppresses printing of numeral and symbols *)
+val without_symbols : ('a -> 'b) -> 'a -> 'b
+
+(* This prints metas as anonymous holes *)
+val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
+
+(* For v8 translation *)
+val set_temporary_implicits_out :
+  (identifier * Impargs.implicits_list) list -> unit