diff options
author | 2016-09-29 17:46:56 +0200 | |
---|---|---|
committer | 2016-09-29 17:46:56 +0200 | |
commit | 2a13b37356cb87de737eaf72b60f337c90913ef9 (patch) | |
tree | f7e408e5ee90f985a2da80da536134b6770f9224 /toplevel | |
parent | 14e47506ffabc43c25bf8da108abb6df78b803ad (diff) | |
parent | 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 (diff) |
Merge branch 'bug4723' into v8.6
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/vernacentries.ml | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 382a71629..25d16f91f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -448,7 +448,27 @@ let vernac_notation locality local = (***********) (* Gallina *) -let start_proof_and_print k l hook = start_proof_com k l hook +let start_proof_and_print k l hook = + let inference_hook = + if Flags.is_program_mode () then + let hook env sigma ev = + let tac = !Obligations.default_tactic in + let evi = Evd.find sigma ev in + let env = Evd.evar_filtered_env evi in + try + let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in + if Evarutil.has_undefined_evars sigma concl then raise Exit; + let c, _, ctx = + Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) + concl (Tacticals.New.tclCOMPLETE tac) + in Evd.set_universe_context sigma ctx, c + with Logic_monad.TacticFailure e when Logic.catchable_exception e -> + error "The statement obligations could not be resolved \ + automatically, write a statement definition first." + in Some hook + else None + in + start_proof_com ?inference_hook k l hook let no_hook = Lemmas.mk_hook (fun _ _ -> ()) |