diff options
| author | Pierre-Marie Pédrot | 2016-11-29 16:30:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:44 +0100 |
| commit | d549d9d3d169fbfc5f555e3e4f22f46301161d53 (patch) | |
| tree | 4cb4052135639414c1f46e3f61a2064ed74d94eb /engine | |
| parent | 4e9cebb0641927f11a21cbb50828974f910cfe47 (diff) | |
Do not ask for a normalized goal to get hypotheses and conclusions.
This is now useless as this returns evar-constrs, so that all functions acting
on them should be insensitive to evar-normalization.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 3 | ||||
| -rw-r--r-- | engine/proofview.mli | 8 |
2 files changed, 2 insertions, 9 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 0a18cf191b..71e9acc88e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -999,9 +999,6 @@ module Goal = struct let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = goal_extra sigma self - let raw_concl { concl=concl } = concl - - let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; diff --git a/engine/proofview.mli b/engine/proofview.mli index 025e3de205..4f662b2948 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -485,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 -> constr - val hyps : ([ `NF ], 'r) t -> named_context + 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 -> constr - type ('a, 'b) enter = { enter : 'r. ('a, 'r) t -> 'b } |