diff options
| author | Maxime Dénès | 2017-05-28 21:54:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-28 21:54:11 +0200 |
| commit | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (patch) | |
| tree | aea1f671a7486d7449ad6883f08e6e9a2ce4f744 /engine/termops.mli | |
| parent | fe62902764cc52daa985ad03e6f7ac0f8f1c2c4c (diff) | |
| parent | 5cc13770ac2358d583b21f217b8c65d2d5abd850 (diff) | |
Merge PR#678: [coqlib] Move `Coqlib` to `library/`.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index fe6dfb0ce1..58837ba033 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -275,10 +275,6 @@ val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) puns val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment -(** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit -val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set - (** {5 Debug pretty-printers} *) open Evd |