diff options
| author | Emilio Jesus Gallego Arias | 2018-10-11 00:20:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-30 23:14:55 +0100 |
| commit | 3429abee7c572676fa1155bf1620386bdf10d798 (patch) | |
| tree | b85975f0e1e9115ab65902463af9aff356b15c72 /plugins/ltac | |
| parent | acd0c18829a03159c489d908ce8f5f510de2f347 (diff) | |
[vernac] [hooks] Refactor towards optional hooks.
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fee469032c..06783de614 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1998,7 +1998,7 @@ let add_morphism_infer atts m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook; + Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance); ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism atts binders m s n = |