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.

8 files changed, 72 insertions, 14 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 46f0219f9..48bf9149d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -239,10 +239,12 @@ let interp_elimination_sort = function
   | GSet  -> InSet
   | GType _ -> InType
 
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
 type inference_flags = {
   use_typeclasses : bool;
   use_unif_heuristics : bool;
-  use_hook : (env -> evar_map -> evar -> constr) option;
+  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
@@ -272,7 +274,7 @@ let apply_inference_hook hook evdref pending =
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
       try
-        let c = hook sigma evk in
+        let sigma, c = hook sigma evk in
         Evd.define evk c sigma
       with Exit ->
         sigma
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 824bb11aa..eead48a54 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -47,10 +47,12 @@ val empty_lvar : ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
 type inference_flags = {
   use_typeclasses : bool;
   use_unif_heuristics : bool;
-  use_hook : (env -> evar_map -> evar -> constr) option;
+  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e4bae2012..a3ece1913 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -161,11 +161,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
-  let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
+  let ce, status, univs =
+    build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
   let ce =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
     else { ce with
@@ -232,8 +233,9 @@ let solve_by_implicit_tactic env sigma evk =
       (try
         let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
         if Evarutil.has_undefined_evars sigma c then raise Exit;
-        let (ans, _, _) = 
+        let (ans, _, ctx) =
 	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
-        ans
+        let sigma = Evd.set_universe_context sigma ctx in
+        sigma, ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 666730e1a..ea604e08e 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -167,7 +167,8 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
   types -> unit Proofview.tactic -> 
-  Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
+  Safe_typing.private_constants Entries.definition_entry * bool *
+    Evd.evar_universe_context
 
 val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
@@ -189,5 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-(* FIXME: interface: it may incur some new universes etc... *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr
+val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 50f2b82c3..bf10b9133 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 f751598f0..904cdeef4 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 : 
diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v
new file mode 100644
index 000000000..888481210
--- /dev/null
+++ b/test-suite/bugs/closed/4723.v
@@ -0,0 +1,28 @@
+
+Require Coq.Program.Tactics.
+
+Record Matrix (m n : nat).
+
+Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q):
+  Matrix (m*p) (n*q). Admitted.
+
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Ltac Obligation Tactic := admit.
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Axiom cheat : forall {A}, A.
+Obligation Tactic := apply cheat.
+
+Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+admit.
+Admitted.
\ No newline at end of file
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 48a85b709..6723a8b48 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 use_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 use_hook k l hook
 
 let no_hook = Lemmas.mk_hook (fun _ _ -> ())