From ae43495dee6e3f4ab407a49050ea2546ab6bd428 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Aug 2017 16:36:52 +0200
Subject: primproj: fix bug 5245, hnf on proj with simpl never flag.

---
 pretyping/tacred.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 76f35f76f5..708788ab87 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -557,6 +557,12 @@ let match_eval_ref_value env sigma constr stack =
       Some (EConstr.of_constr (constant_value_in env (sp, u)))
     else
       None
+  | Proj (p, c) when not (Projection.unfolded p) ->
+     reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+        (lazy (EConstr.to_constr sigma (applist (constr,stack))));
+     if is_evaluable env (EvalConstRef (Projection.constant p)) then
+       Some (mkProj (Projection.unfold p, c))
+     else None
   | Var id when is_evaluable env (EvalVarRef id) -> 
      env |> lookup_named id |> NamedDecl.get_value
   | Rel n ->
-- 
cgit v1.2.3