diff options
| author | Emilio Jesus Gallego Arias | 2019-10-30 15:25:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-30 15:25:19 +0100 |
| commit | 6b13decaa6ca82ce10566121fb38a12072ab2a0c (patch) | |
| tree | 2106cade4e1576fce5c7312f6eb518a4f65319cf /vernac | |
| parent | dbcdc4e53758339d2a7eb96d19fbcffeb143154d (diff) | |
| parent | be4ebad76e7cb132fb890769fcc6a83a781c8522 (diff) | |
Merge PR #10973: Remove dead code in save_remaining_recthms
Ack-by: JasonGross
Reviewed-by: ejgallego
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 7010aa8c6d..1a995c5c7b 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 |