diff options
| author | Gaëtan Gilbert | 2019-10-26 10:25:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-26 15:07:15 +0200 |
| commit | be4ebad76e7cb132fb890769fcc6a83a781c8522 (patch) | |
| tree | 34927152331a9e96b514a0424370917582b29d1e /vernac | |
| parent | f7659e6c5d197ddeff8509a4aab40316534b3a12 (diff) | |
Remove dead code in save_remaining_recthms
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 15 |
1 files changed, 3 insertions, 12 deletions
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 |