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 | |
| parent | f7659e6c5d197ddeff8509a4aab40316534b3a12 (diff) | |
Remove dead code in save_remaining_recthms
| -rw-r--r-- | test-suite/success/Fixpoint.v | 4 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 15 |
2 files changed, 7 insertions, 12 deletions
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 81c9763ccd..ce3fddf249 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -96,10 +96,14 @@ Section visibility. Let Fixpoint by_proof (n:nat) : True. Proof. exact I. Defined. + + Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool. + Admitted. End visibility. Fail Check imm. Fail Check by_proof. +Check bla. Check bli. Module Import mod_local. Fixpoint imm_importable (n:nat) : True := I. 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 |