From 98da9fdce866728f93bc7cb690275f5559aa9bae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Apr 2017 20:37:15 +0200
Subject: Removing various tactic compatibility layers in core tactics.

---
 plugins/ltac/rewrite.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac/rewrite.ml')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600c..12a1566e20 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2197,7 +2197,8 @@ let setoid_transitivity c =
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
-  Proofview.V82.tactic (fun gl ->
+  let open Tacmach.New in
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let ctype = pf_unsafe_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum sigma ctype in
@@ -2211,11 +2212,10 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-   Proofview.V82.of_tactic
     (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
       (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
-      gl)
+  end }
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/rewrite.ml')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 12a1566e20..9a1615d3f2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -39,7 +39,7 @@ open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 
 (** Typeclass-based generalized rewriting. *)
 
-- 
cgit v1.2.3


From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 27 Apr 2017 21:58:52 +0200
Subject: Post-rebase warnings (unused opens and 2 unused values)

---
 plugins/ltac/rewrite.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ltac/rewrite.ml')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9a1615d3f2..5630a2d7b6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
 open Vars
 open Reduction
 open Tacticals.New
-open Tacmach
 open Tactics
 open Pretype_errors
 open Typeclasses
-- 
cgit v1.2.3