diff options
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index d60412c0c..47e806929 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1719,8 +1719,10 @@ end = struct (* {{{ *) match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> + let t = EConstr.of_constr t in let t = Evarutil.nf_evar sigma t in - if Evarutil.is_ground_term sigma (EConstr.of_constr t) then + if Evarutil.is_ground_term sigma t then + let t = EConstr.Unsafe.to_constr t in RespBuiltSubProof (t, Evd.evar_universe_context sigma) else CErrors.user_err ~hdr:"STM" (str"The solution is not ground") end) () |