diff options
Diffstat (limited to 'contrib/correctness/pmisc.mli')
-rw-r--r-- | contrib/correctness/pmisc.mli | 81 |
1 files changed, 0 insertions, 81 deletions
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli deleted file mode 100644 index 9d96467f..00000000 --- a/contrib/correctness/pmisc.mli +++ /dev/null @@ -1,81 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -(* Certification of Imperative Programs / Jean-Christophe Filliātre *) - -(* $Id: pmisc.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Term -open Ptype -open Topconstr - -(* Some misc. functions *) - -val reraise_with_loc : Util.loc -> ('a -> 'b) -> 'a -> 'b - -val list_of_some : 'a option -> 'a list -val difference : 'a list -> 'a list -> 'a list - -val at_id : identifier -> string -> identifier -val un_at : identifier -> identifier * string -val is_at : identifier -> bool - -val result_id : identifier -val adr_id : identifier -> identifier - -val renaming_of_ids : identifier list -> identifier list - -> (identifier * identifier) list * identifier list - -val reset_names : unit -> unit -val pre_name : name -> identifier -val post_name : name -> identifier -val inv_name : name -> identifier -val test_name : name -> identifier -val bool_name : unit -> identifier -val var_name : name -> identifier -val phi_name : unit -> identifier -val for_name : unit -> identifier -val label_name : unit -> string - -val id_of_name : name -> identifier - -(* CIC terms *) - -val isevar : constr - -val subst_in_constr : (identifier * identifier) list -> constr -> constr -val subst_in_ast : (identifier * identifier) list -> constr_expr -> constr_expr -val subst_ast_in_ast : - (identifier * constr_expr) list -> constr_expr -> constr_expr -val real_subst_in_constr : (identifier * constr) list -> constr -> constr - -val constant : string -> constr -val coq_constant : string list -> string -> kernel_name -val conj : constr -> constr -> constr - -val coq_true : constr -val coq_false : constr - -val connective_and : identifier -val connective_or : identifier -val connective_not : identifier -val is_connective : identifier -> bool - -val n_mkNamedProd : constr -> (identifier * constr) list -> constr -val n_lambda : constr -> (identifier * constr) list -> constr -val abstract : (identifier * constr) list -> constr -> constr - -val type_v_knsubst : substitution -> type_v -> type_v -val type_c_knsubst : substitution -> type_c -> type_c - -(* for debugging purposes *) - -val deb_mess : Pp.std_ppcmds -> unit -val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit - |