From cad3fa50357d97e309e9d4fc2a877991c83649d8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 10 Jun 2016 01:34:06 +0200
Subject: Document new Hint Mode option.

---
 engine/evarutil.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index c5dfe30332..4506fddb5f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -192,6 +192,7 @@ let head_evar =
     | Case (_,_,c,_) -> hrec c
     | App (c,_)      -> hrec c
     | Cast (c,_,_)   -> hrec c
+    | Proj (p, c)    -> hrec c
     | _              -> raise NoHeadEvar
   in
   hrec
-- 
cgit v1.2.3