diff options
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 55c8b1452c..8aa459729c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -221,12 +221,12 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in + let k = IsAssumption Conjectural in match body with | None -> (match locality with | Discharge -> let impl = false in (* copy values from Vernacentries *) - let k = IsAssumption Conjectural in let univs = match univs with | Polymorphic_const_entry univs -> (* What is going on here? *) @@ -237,7 +237,6 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_, let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> - let k = IsAssumption Conjectural in let local = match locality with | Local -> true | Global -> false |