https://github.com/EasyCrypt/easycrypt
Revision 266d5c905a90855b639af7d9af6d1975a33fa924 authored by Benjamin Gregoire on 23 June 2014, 14:28:40 UTC, committed by Benjamin Gregoire on 23 June 2014, 14:28:50 UTC
1 parent ea70757
Tip revision: 266d5c905a90855b639af7d9af6d1975a33fa924 authored by Benjamin Gregoire on 23 June 2014, 14:28:40 UTC
Add trivial module in Pair
Add trivial module in Pair
Tip revision: 266d5c9
ecSection.mli
(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B license *)
(* -------------------------------------------------------------------- *)
open EcSymbols
open EcIdent
open EcPath
open EcFol
open EcModules
type locals
(* -------------------------------------------------------------------- *)
val env_of_locals : locals -> EcEnv.env
val items_of_locals : locals -> EcTheory.ctheory_item list
val is_local : [`Lemma | `Module] -> path -> locals -> bool
val is_mp_local : mpath -> locals -> bool
val form_use_local : form -> locals -> bool
val module_use_local_or_abs : module_expr -> locals -> bool
val abstracts : locals -> (EcIdent.t * (module_type * mod_restr)) list * Sid.t
val generalize : EcEnv.env -> locals -> form -> form
(* -------------------------------------------------------------------- *)
type t
exception NoSectionOpened
val initial : t
val in_section : t -> bool
val enter : EcEnv.env -> symbol option -> t -> t
val exit : t -> locals * t
val path : t -> symbol option * path
val opath : t -> (symbol option * path) option
val locals : t -> locals
val olocals : t -> locals option
type lvl = [`Local | `Global] * [`Axiom | `Lemma]
val add_local_mod : path -> t -> t
val add_lemma : path -> lvl -> t -> t
val add_item : EcTheory.ctheory_item -> t -> t
val add_abstract : EcIdent.t -> (module_type * mod_restr) -> t -> t
Computing file changes ...