From 7edf54baf92f219e4a5307c4cb2563b0e7bda070 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 18 Jul 2017 11:26:08 +0200
Subject: Removing default evar-normalization for ARGUMENT EXTEND.

This fixes bug 5650: evar (x : Prop) should not be slow.
---
 grammar/argextend.mlp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 643b6277a..12b7b171b 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -137,7 +137,8 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
       let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
       <:expr<
         let f = $lid:f$ in
-        fun ist v -> Ftactic.nf_enter (fun gl ->
+        fun ist v -> Ftactic.enter (fun gl ->
+          let gl = Proofview.Goal.assume gl in
           let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in
           let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in
           Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v)
-- 
cgit v1.2.3