diff options
| author | Maxime Dénès | 2020-06-16 00:09:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-23 12:09:04 +0200 |
| commit | f67a09a9201916066ed8c9ece073232317e75a8d (patch) | |
| tree | 5a7af13f9d800ce5c819bc32e58b99d9e42af6c6 | |
| parent | 700918ada1c864c900bdc065d39c4b16d2a47500 (diff) | |
Fix #4459 by improving `par:` error message
| -rw-r--r-- | stm/stm.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b72cee7a9d..943c83ecd3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1932,8 +1932,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all is_ground) Evd.(evar_context g)) then - CErrors.user_err ~hdr:"STM" Pp.(strbrk("the par: goal selector supports ground "^ - "goals only")) + CErrors.user_err ~hdr:"STM" Pp.(strbrk("The par: goal selector does not support goals with existential variables")) else begin let (i, ast) = r_ast in PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p); @@ -1950,10 +1949,15 @@ end = struct (* {{{ *) | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> let t = Evarutil.nf_evar sigma t in - if Evarutil.is_ground_term sigma t then + let evars = Evarutil.undefined_evars_of_term sigma t in + if Evar.Set.is_empty evars then let t = EConstr.Unsafe.to_constr t in RespBuiltSubProof (t, Evd.evar_universe_context sigma) - else CErrors.user_err ~hdr:"STM" Pp.(str"The solution is not ground") + else + CErrors.user_err ~hdr:"STM" + Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++ + str" solves the goal and leaves no unresolved existential variables. The following" ++ + str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars)) end) () with e when CErrors.noncritical e -> RespError (CErrors.print e) |