diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 11e9dc16c..19658806c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -449,7 +449,7 @@ let start_proof_and_print k l hook = let evi = Evarutil.nf_evar_info sigma evi in let env = Evd.evar_filtered_env evi in try - let concl = EConstr.of_constr evi.Evd.evar_concl in + let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && Evarutil.is_ground_term sigma concl) then raise Exit; |