From 5cc2882ffaadb92a711297799392d57c13e1895c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 23 Nov 2008 07:55:27 +0000
Subject: Minor improvement to commit 11619

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11620 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES                   | 2 +-
 toplevel/vernacentries.ml | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index e0012e8326..ffae4eb00f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -43,7 +43,6 @@ Language
   As a consequence, Acc_rect has now a more direct proof [possible source
   of easily fixed incompatibility in case of manual definition of a recursor
   in a recursive singleton inductive type].
-- Specific sort constraints on Record now taken into account.
 
 Vernacular commands
 
@@ -82,6 +81,7 @@ Vernacular commands
 - "Declare ML Module" now allows to import .cmxs files when Coq is
   compiled in native code with a version of OCaml that supports native
   Dynlink (>= 3.11).
+- Specific sort constraints on Record now taken into account.
 
 Libraries (DOC TO CHECK)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 36d1e0175e..5f5dab6146 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -377,8 +377,6 @@ let vernac_record k finite struc binders sort nameopt cfs =
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
 	Dumpglob.dump_definition lid false "constr"; id in
-  let sigma = Evd.empty in
-  let env = Global.env() in
     if Dumpglob.dump () then (
       Dumpglob.dump_definition (snd struc) false "rec";
       List.iter (fun ((_, x), _) ->
-- 
cgit v1.2.3