aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--proofs/pfedit.ml10
-rw-r--r--proofs/pfedit.mli6
-rw-r--r--stm/lemmas.ml6
-rw-r--r--stm/lemmas.mli4
-rw-r--r--test-suite/bugs/closed/4723.v28
-rw-r--r--toplevel/vernacentries.ml22
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 _ _ -> ())
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 10:53:46 +0000