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.
---
 parsing/g_proofs.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 422384f3dc..b0ff8b64f2 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -134,6 +134,8 @@ GEXTEND Gram
       | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ]
   ;
   mode:
-    [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ]
+    [ [ l = LIST1 [ "+" -> ModeInput
+                  | "!" -> ModeNoHeadEvar
+                  | "-" -> ModeOutput ] -> l ] ]
   ;
 END
-- 
cgit v1.2.3