diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-13 11:17:00 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-13 11:17:00 +0100 |
| commit | 19d4ba5fa2ff8827f86d00df95a88e3f5cbdfd10 (patch) | |
| tree | 47b48811cca0634dfdb6df780e13b3809903e852 /kernel | |
| parent | f6cc1ab4fcc26e2b0ed9186ee9a3caca7a123d97 (diff) | |
| parent | c0e99b45a97aa0d506e32d1daeb594c372ea82fa (diff) | |
Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5f501bff1..9b864440d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -223,9 +223,8 @@ let rec unzip ctx j = unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let feedback_completion_typecheck = - let open Feedback in Option.iter (fun state_id -> - feedback ~id:state_id Feedback.Complete) + Feedback.feedback ~id:state_id Feedback.Complete) let abstract_constant_universes = function | Monomorphic_const_entry uctx -> |