From 6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 14:23:11 +0200
Subject: More precise explanation when a notation is not reversible for
 printing.

---
 interp/notation_ops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.mli')

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 0904a4ea3e..80348c78ee 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -29,7 +29,7 @@ val ldots_var : Id.t
     bound by the notation; also interpret recursive patterns           *)
 
 val notation_constr_of_glob_constr : notation_interp_env ->
-  glob_constr -> notation_constr * reversibility_flag
+  glob_constr -> notation_constr * reversibility_status
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
-- 
cgit v1.2.3