diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-11 16:00:04 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-12 20:31:51 +0100 |
| commit | 68935660fbfdec2e357e123ed999073ed3b8fc26 (patch) | |
| tree | 572f6e04973aa682358ad0557769c0980a48cc66 /proofs/clenv.mli | |
| parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) | |
[engine] Remove ghost parameter from `Proofview.Goal.t`
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9a2026dd3..c894b9dc9 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -41,10 +41,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -val mk_clenv_from : 'a Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : - 'a Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : 'a Proofview.Goal.t -> EConstr.constr -> clausenv + Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) @@ -66,7 +66,7 @@ val old_clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv val clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> 'a Proofview.Goal.t -> clausenv + ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv val clenv_dependent : clausenv -> metavariable list |