diff options
| -rw-r--r-- | kernel/entries.mli | 7 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 7 | ||||
| -rw-r--r-- | proofs/proofview.ml | 28 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4863.v | 32 |
4 files changed, 64 insertions, 10 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index f94068f31..8e8e97d61 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -97,7 +97,12 @@ type module_entry = | MExpr of module_params_entry * module_struct_entry * module_struct_entry option -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type seff_env = + [ `Nothing + (* The proof term and its universes. + Same as the constant_body's but not in an ephemeron *) + | `Opaque of Constr.t * Univ.universe_context_set ] type side_eff = | SEsubproof of constant * Declarations.constant_body * seff_env diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 927278965..8b28cd87b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -222,13 +222,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) -let constant_entry_of_private_constant = function - | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> - [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ] - | { Entries.eff = Entries.SEscheme (l,_) } -> - List.map (fun (_,kn,cb,eff_env) -> - kn, Term_typing.constant_entry_of_side_effect cb eff_env) l - let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in { Entries.from_env = CEphemeron.create env.revstruct; diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ae7e2b79a..91905be62 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1071,6 +1071,23 @@ struct let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () + (* Get the side-effect's constant declarations to update the monad's + * environmnent *) + let add_if_undefined kn cb env = + try ignore(Environ.lookup_constant kn env); env + with Not_found -> Environ.add_constant kn cb env + + (* Add the side effects to the monad's environment, if not already done. *) + let add_side_effect env = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + add_if_undefined kn cb env + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.fold_left (fun env (_,kn,cb,eff_env) -> + add_if_undefined kn cb env) env l + + let add_side_effects env effects = + List.fold_left (fun env eff -> add_side_effect env eff) env effects + let refine ?(unsafe = true) f = Goal.enter begin fun gl -> let sigma = Goal.sigma gl in let env = Goal.env gl in @@ -1083,6 +1100,10 @@ struct let (sigma, c) = f (Evd.reset_future_goals sigma) in let evs = Evd.future_goals sigma in let evkmain = Evd.principal_future_goal sigma in + (** Redo the effects in sigma in the monad's env *) + let privates_csts = Evd.eval_side_effects sigma in + let sideff = Safe_typing.side_effects_of_private_constants privates_csts in + let env = add_side_effects env sideff in (** Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in @@ -1109,8 +1130,11 @@ struct let comb = undefined sigma (CList.rev evs) in let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> - Pv.modify (fun ps -> { ps with solution = sigma; comb; }) + InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ + Hook.get pr_constrv env sigma c)))) >> + (** We reset the logical environment extended with the effects. *) + Env.set (Environ.reset_context env) >> + Pv.modify (fun ps -> { ps with solution = sigma; comb; }) end (** Useful definitions *) diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v new file mode 100644 index 000000000..e884355fd --- /dev/null +++ b/test-suite/bugs/closed/4863.v @@ -0,0 +1,32 @@ +Require Import Classes.DecidableClass. + +Inductive Foo : Set := +| foo1 | foo2. + +Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. +Proof. + intros P H. + refine (Build_Decidable _ (if H then true else false) _). + intuition congruence. +Qed. + +Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances. + +Goal forall (a b : Foo), {a=b}+{a<>b}. +intros. +abstract (abstract (decide equality)). (*abstract works here*) +Qed. + +Check ltac:(abstract (exact I)) : True. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. typeclasses eauto. typeclasses eauto. Qed. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. +refine _. +refine _. +Defined. +(*fails*) |