From bc04d3196a62a52caca96014448b7b966baedd0c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 16 Jul 2019 14:38:44 +0200
Subject: Move unfold_side_flags CClosure -> Tacred internals

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

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 6fdceb929a..866c0da555 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1103,6 +1103,15 @@ let string_of_evaluable_ref env = function
       string_of_qualid
         (Nametab.shortest_qualid_of_global (vars_of_env env) (GlobRef.ConstRef kn))
 
+(* Removing fZETA for finer behaviour would break many developments *)
+let unfold_side_flags = RedFlags.[fBETA;fMATCH;fFIX;fCOFIX;fZETA]
+let unfold_side_red = RedFlags.(mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA])
+let unfold_red kn =
+  let flag = match kn with
+    | EvalVarRef id -> RedFlags.fVAR id
+    | EvalConstRef kn -> RedFlags.fCONST kn in
+  RedFlags.mkflags (flag::unfold_side_flags)
+
 let unfold env sigma name c =
   if is_evaluable env name then
     clos_norm_flags (unfold_red name) env sigma c
-- 
cgit v1.2.3