From be4ebad76e7cb132fb890769fcc6a83a781c8522 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 26 Oct 2019 10:25:16 +0200
Subject: Remove dead code in save_remaining_recthms

---
 vernac/lemmas.ml | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e49277c51b..d66401507e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -17,7 +17,6 @@ open Pp
 open Names
 open Constr
 open Declareops
-open Entries
 open Nameops
 open Pretyping
 open Termops
@@ -258,17 +257,9 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect
     let open DeclareDef in
     (match scope with
      | Discharge ->
-       let impl = Glob_term.Explicit in
-       let univs = match univs with
-         | Polymorphic_entry (_, univs) ->
-           (* What is going on here? *)
-           Univ.ContextSet.of_context univs
-         | Monomorphic_entry univs -> univs
-       in
-       let () = Declare.declare_universe_context ~poly univs in
-       let c = Declare.SectionLocalAssum {typ=t_i; impl} in
-       let () = Declare.declare_variable ~name ~kind c in
-       GlobRef.VarRef name, impargs
+       (* Let Fixpoint + Admitted gets turned into axiom so scope is Global,
+          see finish_admitted *)
+       assert false
      | Global local ->
        let kind = Decls.(IsAssumption Conjectural) in
        let decl = Declare.ParameterEntry (None,(t_i,univs),None) in
-- 
cgit v1.2.3