aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 36d1e0175..5f5dab614 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), _) ->