diff options
| author | Emilio Jesus Gallego Arias | 2020-06-29 15:26:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-08 15:12:46 +0200 |
| commit | 4413a1fb74fc2fd33176e5983a9977f9e28218d9 (patch) | |
| tree | a8ce1ab25d8073ad8d1a5bb37bbbe5a03c833676 | |
| parent | a164eaafad33ccbc2b0bdbb75147a54ebe3a9848 (diff) | |
[declare] Allow obligations update on equations closing hook.
This is also needed in equations.
| -rw-r--r-- | vernac/declare.ml | 10 | ||||
| -rw-r--r-- | vernac/declare.mli | 2 |
2 files changed, 6 insertions, 6 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 37612a9f9b..e19eca9a1c 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1317,7 +1317,7 @@ module Proof_ending = struct | End_obligation of Obls_.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } | End_equations of - { hook : Constant.t list -> Evd.evar_map -> unit + { hook : pm:Obls_.State.t -> Constant.t list -> Evd.evar_map -> Obls_.State.t ; i : Id.t ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list ; sigma : Evd.evar_map @@ -2005,7 +2005,7 @@ let finish_derived ~f ~name ~entries = let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in [GlobRef.ConstRef ct] -let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = +let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = let obls = ref 1 in let sigma, recobls = @@ -2022,8 +2022,8 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = sigma, cst) sigma0 types proof_obj.entries in - hook recobls sigma; - List.map (fun cst -> GlobRef.ConstRef cst) recobls + let pm = hook ~pm recobls sigma in + pm, List.map (fun cst -> GlobRef.ConstRef cst) recobls let check_single_entry { entries; uctx } label = match entries with @@ -2044,7 +2044,7 @@ let finalize_proof ~pm proof_obj proof_info = pm, finish_derived ~f ~name ~entries:proof_obj.entries | End_equations { hook; i; types; sigma } -> let kind = proof_info.Proof_info.info.Info.kind in - pm, finish_proved_equations ~kind ~hook i proof_obj types sigma + finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma let err_save_forbidden_in_place_of_qed () = CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") diff --git a/vernac/declare.mli b/vernac/declare.mli index 9d9516d963..d302f68153 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -182,7 +182,7 @@ module Proof : sig val start_equations : name:Id.t -> info:Info.t - -> hook:(Constant.t list -> Evd.evar_map -> unit) + -> hook:(pm:OblState.t -> Constant.t list -> Evd.evar_map -> OblState.t) -> types:(Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list -> Evd.evar_map -> Proofview.telescope |