diff options
| author | Maxime Dénès | 2015-07-02 16:16:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-07-02 16:16:46 +0200 |
| commit | 27de0f2d7e5cd0cc4b221413dfe3c7b739104350 (patch) | |
| tree | a42625106f71295ebc2011b797603cd1b3b8ec83 /kernel/names.mli | |
| parent | a28d9981e5baf812de14e62de8d904e545e804e5 (diff) | |
| parent | 44f45f58dc0a169286c9fcfa7d2edbc8bc04673b (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 92ee58f260..7cc4443752 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -652,6 +652,10 @@ module Projection : sig val compare : t -> t -> int val map : (constant -> constant) -> t -> t + + val to_string : t -> string + val print : t -> Pp.std_ppcmds + end type projection = Projection.t |