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.ml | |
| parent | fe62902764cc52daa985ad03e6f7ac0f8f1c2c4c (diff) | |
| parent | 5cc13770ac2358d583b21f217b8c65d2d5abd850 (diff) | |
Merge PR#678: [coqlib] Move `Coqlib` to `library/`.
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 22 |
1 files changed, 0 insertions, 22 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 |