aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-03-04 17:40:10 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-03-04 17:40:48 +0100
commitb98e4857a13a4014c65882af5321ebdb09f41890 (patch)
treec4968e85483866529cc8f4e9a37da28470548d90 /kernel/term_typing.ml
parent78b5670a0a1cf7ba31acabe710b311bf13df8745 (diff)
Rename Ephemeron -> CEphemeron.
Fixes compilation of Coq with OCaml 4.03 beta 1.
Diffstat (limited to 'kernel/term_typing.ml')
-rw-r--r--kernel/term_typing.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 510f43542..fdbd1e3b1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -126,14 +126,14 @@ let check_signatures curmb sl =
| None -> None, None
| Some curmb ->
try
- let mb = Ephemeron.get mb in
+ let mb = CEphemeron.get mb in
match sl with
| None -> sl, None
| Some n ->
if List.length mb >= how_many && CList.skipn how_many mb == curmb
then Some (n + how_many), Some mb
else None, None
- with Ephemeron.InvalidKey -> None, None in
+ with CEphemeron.InvalidKey -> None, None in
let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
sl