Using non-normalized goals in tactic interpretation.

6 files changed, 86 insertions, 81 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index adeb507416..a9146a96a8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -253,4 +253,11 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     List.hd hyps
 
+  let pf_nf_concl gl =
+    (** We normalize the conclusion just after *)
+    let gl = Proofview.Goal.assume gl in
+    let concl = Proofview.Goal.concl gl in
+    let sigma = Proofview.Goal.sigma gl in
+    nf_evar sigma concl
+
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 07639f475d..9a53560b6b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -143,4 +143,6 @@ module New : sig
   val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
   val pf_get_hyp_typ        : identifier -> [ `NF ] Proofview.Goal.t -> types
   val pf_last_hyp           : [ `NF ] Proofview.Goal.t -> named_declaration
+
+  val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
 end
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 13c188c79e..9c8412454d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -38,30 +38,32 @@ let absurd c = Proofview.V82.tactic (absurd c)
 
 (* Contradiction *)
 
+(** [f] does not assume its argument to be [nf_evar]-ed. *)
 let filter_hyp f tac =
   let rec seek = function
     | [] -> Proofview.tclZERO Not_found
     | (id,_,t)::rest when f t -> tac id
     | _::rest -> seek rest in
-  Proofview.Goal.enter begin fun gl ->
-    let hyps = Proofview.Goal.hyps gl in
+  Proofview.Goal.raw_enter begin fun gl ->
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     seek hyps
   end
 
 let contradiction_context =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
       | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
       | (id,_,typ)::rest ->
+          let typ = nf_evar sigma typ in
 	  let typ = whd_betadeltaiota env sigma typ in
 	  if is_empty_type typ then
 	    simplest_elim (mkVar id)
 	  else match kind_of_term typ with
 	  | Prod (na,t,u) when is_empty_type u ->
 	      (Proofview.tclORELSE
-                 (Proofview.Goal.enter begin fun gl ->
+                 (Proofview.Goal.raw_enter begin fun gl ->
                    let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
 	           filter_hyp (fun typ -> is_conv_leq typ t)
 		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
@@ -72,13 +74,15 @@ let contradiction_context =
                  end)
 	  | _ -> seek_neg rest
     in
-    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     seek_neg hyps
   end
 
 let is_negation_of env sigma typ t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
-    | Prod (na,t,u) -> is_empty_type u && is_conv_leq env sigma typ t
+    | Prod (na,t,u) ->
+      let u = nf_evar sigma u in
+      is_empty_type u && is_conv_leq env sigma typ t
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9816162460..3d9091189f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1432,7 +1432,7 @@ and interp_atomic ist tac =
   match tac with
   (* Basic tactics *)
   | TacIntroPattern l ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let patterns = interp_intro_pattern_list_as_list ist env l in
         Tactics.intro_patterns patterns
@@ -1443,7 +1443,7 @@ and interp_atomic ist tac =
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
   | TacIntroMove (ido,hto) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let mloc = interp_move_location ist env hto in
         Tactics.intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
@@ -1474,7 +1474,7 @@ and interp_atomic ist tac =
           gl
       end
   | TacApply (a,ev,cb,cl) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         try (* interp_open_constr_with_bindings_loc can raise exceptions *)
@@ -1485,7 +1485,7 @@ and interp_atomic ist tac =
             | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
             | Some cl ->
                 (fun l ->
-                  Proofview.Goal.enter begin fun gl ->
+                  Proofview.Goal.raw_enter begin fun gl ->
                     let env = Proofview.Goal.env gl in
                     let (id,cl) = interp_in_hyp_as ist env cl in
                     Tactics.apply_in a ev id l cl
@@ -1494,7 +1494,7 @@ and interp_atomic ist tac =
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
   | TacElim (ev,cb,cbo) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in 
         try (* interpretation functions may raise exceptions *)
@@ -1512,7 +1512,7 @@ and interp_atomic ist tac =
           gl
       end
   | TacCase (ev,cb) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
@@ -1527,7 +1527,7 @@ and interp_atomic ist tac =
           gl
       end
   | TacFix (idopt,n) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         Proofview.V82.tactic (Tactics.fix (Option.map (interp_fresh_ident ist env) idopt) n)
       end
@@ -1546,7 +1546,7 @@ and interp_atomic ist tac =
           gl
       end
   | TacCofix idopt ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         Proofview.V82.tactic (Tactics.cofix (Option.map (interp_fresh_ident ist env) idopt))
       end
@@ -1566,11 +1566,11 @@ and interp_atomic ist tac =
       end
   | TacCut c ->
       let open Proofview.Notations in
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         new_interp_type ist c gl >>= Tactics.cut
       end
   | TacAssert (t,ipat,c) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         try (* intrerpreation function may raise exceptions *)
@@ -1635,7 +1635,7 @@ and interp_atomic ist tac =
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         Auto.h_trivial ~debug
@@ -1643,7 +1643,7 @@ and interp_atomic ist tac =
 	  (Option.map (List.map (interp_hint_base ist)) l)
       end
   | TacAuto (debug,n,lems,l) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
@@ -1704,7 +1704,7 @@ and interp_atomic ist tac =
 	(Elim.h_decompose l c_interp)
       end
   | TacSpecialize (n,cb) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
@@ -1752,21 +1752,21 @@ and interp_atomic ist tac =
 
   (* Constructors *)
   | TacLeft (ev,bl) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
         Tacticals.New.tclWITHHOLES ev (Tactics.left_with_bindings ev) sigma bl
       end
   | TacRight (ev,bl) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
         Tacticals.New.tclWITHHOLES ev (Tactics.right_with_bindings ev) sigma bl
       end
   | TacSplit (ev,_,bll) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
@@ -1775,7 +1775,7 @@ and interp_atomic ist tac =
   | TacAnyConstructor (ev,t) ->
       Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
   | TacConstructor (ev,n,bl) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
@@ -1815,7 +1815,7 @@ and interp_atomic ist tac =
       end
   | TacChange (Some op,c,cl) ->
       Proofview.V82.nf_evar_goals <*>
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
@@ -1840,7 +1840,7 @@ and interp_atomic ist tac =
   (* Equivalence relations *)
   | TacReflexivity -> Tactics.intros_reflexivity
   | TacSymmetry c ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let cl = interp_clause ist env c in
         Tactics.intros_symmetry cl
@@ -1861,7 +1861,7 @@ and interp_atomic ist tac =
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let l = List.map (fun (b,m,c) ->
           let f env sigma = interp_open_constr_with_bindings ist env sigma c in
 	  (b,m,f)) l in
@@ -1892,7 +1892,7 @@ and interp_atomic ist tac =
           dqhyps
       end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let interp_intro_pattern = interp_intro_pattern ist env in
         let hyps = interp_hyp_list ist env idl in
@@ -1903,7 +1903,7 @@ and interp_atomic ist tac =
           dqhyps
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let (sigma,c_interp) = interp_constr ist env sigma c in
@@ -2056,7 +2056,7 @@ let eval_tactic_ist ist t =
 
 
 let interp_tac_gen lfun avoid_ids debug t =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
@@ -2087,7 +2087,7 @@ let hide_interp global t ot =
     Proofview.tclENV >>= fun env ->
     hide_interp env
   else
-    Proofview.Goal.enter begin fun gl ->
+    Proofview.Goal.raw_enter begin fun gl ->
       hide_interp (Proofview.Goal.env gl)
     end
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index dd344ee3d9..a9d95d241b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -549,15 +549,17 @@ module New = struct
     with Failure _ -> Errors.error "No such assumption."
 
   let nthHypId m gl =
+    (** We only use [id] *)
+    let gl = Proofview.Goal.assume gl in
     let (id,_,_) = nthDecl m gl in
     id
   let nthHyp m gl = 
     mkVar (nthHypId m gl)
 
   let onNthHypId m tac =
-    Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end
+    Proofview.Goal.raw_enter begin fun gl -> tac (nthHypId m gl) end
   let onNthHyp m tac =
-    Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
+    Proofview.Goal.raw_enter begin fun gl -> tac (nthHyp m gl) end
 
   let onLastHypId = onNthHypId 1
   let onLastHyp   = onNthHyp 1
@@ -582,17 +584,17 @@ module New = struct
     None :: List.map Option.make hyps
 
   let tryAllHyps tac =
-    Proofview.Goal.enter begin fun gl ->
+    Proofview.Goal.raw_enter begin fun gl ->
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclFIRST_PROGRESS_ON tac hyps
     end
   let tryAllHypsAndConcl tac =
-    Proofview.Goal.enter begin fun gl ->
+    Proofview.Goal.raw_enter begin fun gl ->
       tclFIRST_PROGRESS_ON tac (fullGoal gl)
     end
 
   let onClause tac cl =
-    Proofview.Goal.enter begin fun gl ->
+    Proofview.Goal.raw_enter begin fun gl ->
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
     end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb7a7b0d98..718c039faa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -188,6 +188,9 @@ let fresh_id_in_env avoid id env =
 let fresh_id avoid id gl =
   fresh_id_in_env avoid id (pf_env gl)
 
+let new_fresh_id avoid id gl =
+  fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
 (**************************************************************)
 (*          Fixpoints and CoFixpoints                         *)
 (**************************************************************)
@@ -422,12 +425,11 @@ let find_name loc decl x gl = match x with
       (* this case must be compatible with [find_intro_names] below. *)
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
-      Tacmach.New.of_old (fresh_id idl (default_id env sigma decl)) gl
-  | IntroBasedOn (id,idl) ->  Tacmach.New.of_old (fresh_id idl id) gl
+      new_fresh_id idl (default_id env sigma decl) gl
+  | IntroBasedOn (id,idl) ->  new_fresh_id idl id gl
   | IntroMustBe id ->
       (* When name is given, we allow to hide a global name *)
-      let hyps = Proofview.Goal.hyps gl in
-      let ids_of_hyps = ids_of_named_context hyps in
+      let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
       let id' = next_ident_away id ids_of_hyps in
       if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
       id'
@@ -453,8 +455,9 @@ let build_intro_tac id dest tac = match dest with
   | dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
 
 let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
-  Proofview.Goal.enter begin fun gl ->
-    let concl = Proofview.Goal.concl gl in
+  Proofview.Goal.raw_enter begin fun gl ->
+    let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    let concl = nf_evar (Proofview.Goal.sigma gl) concl in
     match kind_of_term concl with
     | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
         let name = find_name loc (name,None,t) name_flag gl in
@@ -3085,7 +3088,7 @@ let find_elim_signature isrec elim hyp0 gl =
 let is_functional_induction elim gl =
   match elim with
   | Some elimc ->
-      let scheme = compute_elim_sig ~elimc (pf_type_of gl (fst elimc)) in
+      let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in
       (* The test is not safe: with non-functional induction on non-standard
          induction scheme, this may fail *)
       Option.is_empty scheme.indarg
@@ -3175,9 +3178,9 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
    hypotheses from the context *)
 
 let apply_induction_in_context hyp0 elim indvars names induct_tac =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let concl = Proofview.Goal.concl gl in
+    let concl = Tacmach.New.pf_nf_concl gl in
     let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
     let deps = List.map (on_pi3 refresh_universes_strict) deps in
     let tmpcl = it_mkNamedProd_or_LetIn concl deps in
@@ -3344,16 +3347,16 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	  (induction_with_atomization_of_ind_arg
 	    isrec with_evars elim names (id,lbind) inhyps)
     | _        ->
-        Proofview.Goal.enter begin fun gl ->
+        Proofview.Goal.raw_enter begin fun gl ->
           let defs = Proofview.Goal.sigma gl in
           let env = Proofview.Goal.env gl in
 	  let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
 	        Anonymous in
-          let id = Tacmach.New.of_old (fresh_id [] x) gl in
+          let id = new_fresh_id [] x gl in
 	(* We need the equality name now *)
 	  let with_eq = Option.map (fun eq -> (false,eq)) eqname in
 	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
-          Proofview.Goal.enter begin fun gl ->
+          Proofview.Goal.raw_enter begin fun gl ->
             let env = Proofview.Goal.env gl in
 	    Tacticals.New.tclTHEN
             (* Warning: letin is buggy when c is not of inductive type *)
@@ -3387,13 +3390,13 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 		atomize_list l'
 
 	    | _ ->
-                Proofview.Goal.enter begin fun gl ->
+                Proofview.Goal.raw_enter begin fun gl ->
                 let type_of = Tacmach.New.pf_type_of gl in
 		try (* type_of can raise an exception *)
                 let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
-                let id = Tacmach.New.of_old (fresh_id [] x) gl in
+                let id = new_fresh_id [] x gl in
 		let newl' = List.map (replace_term c (mkVar id)) l' in
 		let _ = newlc:=id::!newlc in
 		let _ = letids:=id::!letids in
@@ -3420,8 +3423,8 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
    args *)
 let induct_destruct isrec with_evars (lc,elim,names,cls) =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
-  Proofview.Goal.enter begin fun gl ->
-  let ifi = Tacmach.New.of_old (is_functional_induction elim) gl in
+  Proofview.Goal.raw_enter begin fun gl ->
+  let ifi = is_functional_induction elim gl in
   if Int.equal (List.length lc) 1 && not ifi then
     (* standard induction *)
     onOpenInductionArg
@@ -3611,18 +3614,21 @@ let dImp cls =
 
 let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
 
+let maybe_betadeltaiota_concl allowred gl =
+  let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = nf_evar sigma concl in
+  if not allowred then concl
+  else
+    let env = Proofview.Goal.env gl in
+    whd_betadeltaiota env sigma concl
+
 let reflexivity_red allowred =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   (* PL: usual reflexivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let concl = if not allowred then Proofview.Goal.concl gl
-    else
-      let c = Proofview.Goal.concl gl in
-      let env = Proofview.Goal.env gl in
-      let sigma = Proofview.Goal.sigma gl in
-      whd_betadeltaiota env sigma c
-  in
+    let concl = maybe_betadeltaiota_concl allowred gl in
     match match_with_equality_type concl with
     | None -> Proofview.tclZERO NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
@@ -3668,19 +3674,11 @@ let match_with_equation c =
     Proofview.tclZERO NoEquationFound
 
 let symmetry_red allowred =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   (* PL: usual symmetry don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let concl =
-    if not allowred then
-      Proofview.Goal.concl gl
-    else
-      let c = Proofview.Goal.concl gl in
-      let env = Proofview.Goal.env gl in
-      let sigma = Proofview.Goal.sigma gl in
-      whd_betadeltaiota env sigma c
-  in
+  let concl = maybe_betadeltaiota_concl allowred gl in
   match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
@@ -3704,7 +3702,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 
 let symmetry_in id =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   let type_of = Tacmach.New.pf_type_of gl in
   try (* type_of can raise an exception *)
   let ctype = type_of (mkVar id) in
@@ -3750,7 +3748,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
 
 (* This is probably not very useful any longer *)
 let prove_transitivity hdcncl eq_kind t =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   let (eq1,eq2) = match eq_kind with
   | MonomorphicLeibnizEq (c1,c2) ->
       mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
@@ -3773,19 +3771,11 @@ let prove_transitivity hdcncl eq_kind t =
   end
 
 let transitivity_red allowred t =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   (* PL: usual transitivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let concl =
-    if not allowred then
-      Proofview.Goal.concl gl
-    else
-      let c = Proofview.Goal.concl gl in
-      let env = Proofview.Goal.env gl in
-      let sigma = Proofview.Goal.sigma gl in
-      whd_betadeltaiota env sigma c
-  in
+  let concl = maybe_betadeltaiota_concl allowred gl in
   match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->