diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 8b4b41219b..a36fae8924 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -32,7 +32,7 @@ open Coercion.Default let pf_env = Refiner.pf_env let pf_hyps = Refiner.pf_hyps let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c -let pf_concl = Tacmach.pf_concl +let pf_concl gls = Goal.V82.concl (Refiner.project gls) (sig_it gls) (******************************************************************) (* Clausal environments *) |