From 8287733d5df1bd673a38e92f23c47e95d1bb7a91 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Sep 2014 21:43:45 +0200
Subject: Putting back normalized goals when entering them.

This should allow tactics after a Goal.enter not to have to renormalize
them uselessly.
---
 tactics/rewrite.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 2c6e7e736a..b67aee7f77 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -33,7 +33,6 @@ open Locus
 open Locusops
 open Decl_kinds
 open Elimschemes
-open Goal
 open Environ
 open Tacinterp
 open Termops
-- 
cgit v1.2.3