From caeba655b78a0107c1988e5377cdd11fa91c5ea2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 7 Nov 2015 22:48:15 +0100
Subject: Experimenting removing strong normalization of the mid-statement in
 tactic cut.

---
 tactics/tactics.ml    | 4 +++-
 theories/Program/Wf.v | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a2275b08fb..c76aeb4a88 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1031,6 +1031,8 @@ let map_induction_arg f = function
 (* tactic "cut" (actually modus ponens) *)
 (****************************************)
 
+let normalize_cut = false
+
 let cut c =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -1049,7 +1051,7 @@ let cut c =
     if is_sort then
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
-      let c = local_strong whd_betaiota sigma c in
+      let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
       Proofview.Refine.refine ~unsafe:true { run = begin fun h ->
         let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
         let Sigma (x, h, q) = Evarutil.new_evar env h c in
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d89919b0a0..6e5919b342 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -89,7 +89,7 @@ Section Measure_well_founded.
   Lemma measure_wf: well_founded MR.
   Proof with auto.
     unfold well_founded.
-    cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a).
+    cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
       intros.
       apply (H (m a))...
     apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
-- 
cgit v1.2.3