diff options
| author | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
| commit | 835be3a05e28eb6e26f703a034f22b2c6c61acaa (patch) | |
| tree | 00ecf04840ba027c3c71f8503d9811c8a5dc1d2e /engine/proofview.mli | |
| parent | 0980dbb1740c8d48d8ff0c516929f27f8cea854d (diff) | |
| parent | 2e6a89238dc7197057d0da80a16f4b4b1e41bfd8 (diff) | |
Merge PR#379: Introducing evar-insensitive constrs
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 294b03dca2..a3b0304b17 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -14,6 +14,7 @@ open Util open Term +open EConstr (** Main state of tactics *) type proofview @@ -43,7 +44,7 @@ val compact : entry -> proofview -> entry * proofview empty [evar_map] (indeed a proof can be triggered by an incomplete pretyping), [init] takes an additional argument to represent the initial [evar_map]. *) -val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview +val init : Evd.evar_map -> (Environ.env * types) list -> entry * proofview (** A [telescope] is a list of environment and conclusion like in {!init}, except that each element may depend on the previous @@ -52,7 +53,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview [evar_map] is threaded in state passing style. *) type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * types * (Evd.evar_map -> constr -> telescope) (** Like {!init}, but goals are allowed to be dependent on one another. Dependencies between goals is represented with the type @@ -484,16 +485,12 @@ module Goal : sig respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : ([ `NF ], 'r) t -> Term.constr - val hyps : ([ `NF ], 'r) t -> Context.Named.t + val concl : ('a, 'r) t -> constr + val hyps : ('a, 'r) t -> named_context val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t val extra : ('a, 'r) t -> Evd.Store.t - (** Returns the goal's conclusion even if the goal is not - normalised. *) - val raw_concl : ('a, 'r) t -> Term.constr - type ('a, 'b) enter = { enter : 'r. ('a, 'r) t -> 'b } |