diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-27 02:37:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-27 22:01:36 +0200 |
| commit | 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 (patch) | |
| tree | 77f792ccddcc48229c08f321666c85debc4b008f /proofs | |
| parent | c33988dafcad14f9f0c10a287d2cfb2790e253c4 (diff) | |
Swapping Context and Constr: defining declarations on constr in Constr.
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 47c9c51ee..7e250faa8 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -93,7 +93,7 @@ type pstate = { pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; - section_vars : Context.Named.t option; + section_vars : Constr.named_context option; proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 9e07ed2d0..854ceaa41 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -126,8 +126,8 @@ 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.lident list -val get_used_variables : unit -> Context.Named.t option + Names.Id.t list -> Constr.named_context * Names.lident list +val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : unit -> UState.universe_decl |