From 875f235dd0413faa34f7d46afc25d2eb90e386e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Sep 2016 17:01:26 +0200
Subject: Fix bug #4723 and FIXME in API for solve_by_tac

This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
---
 stm/lemmas.ml  | 6 ++++--
 stm/lemmas.mli | 4 +++-
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 50f2b82c3b..bf10b91339 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
       start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
-let start_proof_com kind thms hook =
+let start_proof_com use_hook kind thms hook =
   let env0 = Global.env () in
   let levels = Option.map snd (fst (List.hd thms)) in 
   let evdref = ref (match levels with
@@ -459,7 +459,9 @@ let start_proof_com kind thms hook =
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
+    let flags = all_and_fail_flags in
+    let flags = { flags with use_hook } in
+    evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
     let ids = List.map get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index f751598f04..904cdeef4d 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -33,7 +33,9 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
-val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
+val start_proof_com :
+  Pretyping.inference_hook option ->
+  goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-- 
cgit v1.2.3


From 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 14:40:00 +0200
Subject: Cleanup API, making inference_hook optional

---
 stm/lemmas.ml  | 4 ++--
 stm/lemmas.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index bf10b91339..022c89ad9a 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
       start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
-let start_proof_com use_hook kind thms hook =
+let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
   let levels = Option.map snd (fst (List.hd thms)) in 
   let evdref = ref (match levels with
@@ -460,7 +460,7 @@ let start_proof_com use_hook kind thms hook =
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
     let flags = all_and_fail_flags in
-    let flags = { flags with use_hook } in
+    let flags = { flags with use_hook = inference_hook } in
     evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
     let ids = List.map get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 904cdeef4d..39c089be9f 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -34,7 +34,7 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma
   (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
 val start_proof_com :
-  Pretyping.inference_hook option ->
+  ?inference_hook:Pretyping.inference_hook ->
   goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
-- 
cgit v1.2.3