From c81065e5cdc6d803bd67eccf93dc8fbb640c6892 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 22 Nov 2014 20:30:19 +0100
Subject: One more word about "simpl f": avoid "simpl f" to be printed "simpl
 f", at least when f is an evaluable reference.

---
 proofs/redexpr.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index fb501c7a5..386ad70ec 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -183,10 +183,8 @@ let contextualize f g = function
   | Some (occs,c) ->
       let l = Locusops.occurrences_map (List.map out_arg) occs in
       let b,c,h = match c with
-        | Inl r -> true, PRef (global_of_evaluable_reference r),f
-        | Inr c ->
-            let b = if head_style then false else (* compat *) is_reference c in
-            b,c,g in
+        | Inl r -> true,PRef (global_of_evaluable_reference r),f
+        | Inr c -> false,c,f in
       e_red (contextually b (l,c) (fun _ -> h))
   | None -> e_red g
 
-- 
cgit v1.2.3