diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-14 06:57:40 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:23:40 +0100 |
commit | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (patch) | |
tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 /proofs/proof_global.mli | |
parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) |
[located] More work towards using CAst.t
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
Diffstat (limited to 'proofs/proof_global.mli')
-rw-r--r-- | proofs/proof_global.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index fb123fccb..bf35fd659 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t val get_all_proof_names : unit -> Names.Id.t list -val discard : Names.Id.t Loc.located -> unit +val discard : Misctypes.lident -> unit val discard_current : unit -> unit val discard_all : unit -> unit @@ -124,7 +124,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list + Names.Id.t list -> Context.Named.t * Misctypes.lident list val get_used_variables : unit -> Context.Named.t option (** Get the universe declaration associated to the current proof. *) |