From 98703c8247fd86deab2d82a70c22d43797e4a548 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 10 Jun 2016 01:15:38 +0200
Subject: Extend Hint Mode to handle the no-head-evar case

Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.
---
 printing/ppvernac.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f3558054b3..5b73b054dd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -161,6 +161,11 @@ module Make
     | HintsReference r -> pr_reference r
     | HintsConstr c -> pr_c c
 
+  let pr_hint_mode = function
+    | ModeInput -> str"+"
+    | ModeNoHeadEvar -> str"!"
+    | ModeOutput -> str"-"
+
   let pr_hints db h pr_c pr_pat =
     let opth = pr_opt_hintbases db  in
     let pph =
@@ -182,8 +187,8 @@ module Make
         | HintsMode (m, l) ->
           keyword "Mode"
           ++ spc ()
-          ++ pr_reference m ++ spc() ++ prlist_with_sep spc
-            (fun b -> if b then str"+" else str"-") l
+          ++ pr_reference m ++ spc() ++
+            prlist_with_sep spc pr_hint_mode l
         | HintsConstructors c ->
           keyword "Constructors"
           ++ spc() ++ prlist_with_sep spc pr_reference c
-- 
cgit v1.2.3