diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 02:01:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:54 -0400 |
| commit | eb452f9da5a52df0d74f7a433cfe98e31ab4ab15 (patch) | |
| tree | 41c036ee34347b765d42340c615e303b5e9fe201 /vernac | |
| parent | 0e329b81794c582ca845d2fc547bfdefad89a972 (diff) | |
[declare/lemmas] Make inference hook exception-free
This is a step towards cleanup of the `start` lemma path.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e7930cc091..30a1475e60 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -473,11 +473,14 @@ let program_inference_hook env sigma ev = let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && Evarutil.is_ground_term sigma concl) - then raise Exit; - let c, _, _, ctx = - Pfedit.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac - in Evd.set_universe_context sigma ctx, EConstr.of_constr c - with Logic_monad.TacticFailure e when noncritical e -> + then None + else + let c, _, _, ctx = + Pfedit.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac + in + Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c) + with + | Logic_monad.TacticFailure e when noncritical e -> user_err Pp.(str "The statement obligations could not be resolved \ automatically, write a statement definition first.") |