diff options
Diffstat (limited to 'contrib/correctness/prename.mli')
-rw-r--r-- | contrib/correctness/prename.mli | 57 |
1 files changed, 0 insertions, 57 deletions
diff --git a/contrib/correctness/prename.mli b/contrib/correctness/prename.mli deleted file mode 100644 index 1d3ab669..00000000 --- a/contrib/correctness/prename.mli +++ /dev/null @@ -1,57 +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: prename.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names - -(* Abstract type for renamings - * - * Records the names of the mutables objets (ref, arrays) at the different - * moments of the evaluation, called dates - *) - -type t - -type date = string - - -val empty_ren : t -val update : t -> date -> identifier list -> t - (* assign new names for the given variables, associated to a new date *) -val next : t -> identifier list -> t - (* assign new names for the given variables, associated to a new - * date which is generated from an internal counter *) -val push_date : t -> date -> t - (* put a new date on top of the stack *) - -val valid_date : date -> t -> bool -val current_date : t -> date -val all_dates : t -> date list - -val current_var : t -> identifier -> identifier -val current_vars : t -> identifier list -> (identifier * identifier) list - (* gives the current names of some variables *) - -val avoid : t -> identifier list -> t -val fresh : t -> identifier list -> (identifier * identifier) list - (* introduces new names to avoid and renames some given variables *) - -val var_at_date : t -> date -> identifier -> identifier - (* gives the name of a variable at a given date *) -val vars_at_date : t -> date -> identifier list - -> (identifier * identifier) list - (* idem for a list of variables *) - -(* pretty-printers *) - -val pp : t -> Pp.std_ppcmds -val ppr : t -> unit - |