Using non-normalized goals in tactic interpretation.

1 files changed, 24 insertions, 24 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 981616246..3d9091189 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