diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 22 | ||||
| -rw-r--r-- | engine/termops.mli | 4 |
2 files changed, 0 insertions, 26 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 19e62f8e62..ca32c06a75 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1468,25 +1468,3 @@ let env_rel_context_chop k env = let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), ctx1 - -(*******************************************) -(* Functions to deal with impossible cases *) -(*******************************************) -let impossible_default_case = ref None - -let set_impossible_default_clause c = impossible_default_case := Some c - -let coq_unit_judge = - let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in - let na1 = Name (Id.of_string "A") in - let na2 = Name (Id.of_string "H") in - fun () -> - match !impossible_default_case with - | Some fn -> - let (id,type_of_id), ctx = fn () in - make_judge id type_of_id, ctx - | None -> - (* In case the constants id/ID are not defined *) - make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) - (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), - Univ.ContextSet.empty 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 |