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.

---
 intf/notation_term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index cad6f4b821..d1cbb6a33d 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -74,7 +74,7 @@ type interpretation =
     (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
 
-type reversibility_flag = bool
+type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
 
 type notation_interp_env = {
   ninterp_var_type : notation_var_internalization_type Id.Map.t;
-- 
cgit v1.2.3