diff options
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 } |