From 521a7b96c8963428ca0ecb39a22f458bf603ccab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 6 Sep 2014 17:09:51 +0200
Subject: Renaming goal-entering functions.

1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals

This is more uniform with the other functions of Coq.
---
 tactics/contradiction.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tactics/contradiction.ml')

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 4a43b8038..cb1b7d557 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -24,7 +24,7 @@ let mk_absurd_proof t =
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let j = Retyping.get_judgment_of env sigma c in
@@ -47,13 +47,13 @@ let filter_hyp f tac =
     | [] -> Proofview.tclZERO Not_found
     | (id,_,t)::rest when f t -> tac id
     | _::rest -> seek rest in
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     seek hyps
   end
 
 let contradiction_context =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.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
@@ -66,7 +66,7 @@ let contradiction_context =
 	  else match kind_of_term typ with
 	  | Prod (na,t,u) when is_empty_type u ->
 	      (Proofview.tclORELSE
-                 (Proofview.Goal.raw_enter begin fun gl ->
+                 (Proofview.Goal.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'|])))
@@ -89,7 +89,7 @@ let is_negation_of env sigma typ t =
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_type_of gl in
-- 
cgit v1.2.3