diff options
| author | Hugo Herbelin | 2018-10-09 19:44:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-15 13:54:12 +0200 |
| commit | 7c85593cc820e7480248b9308b95f5808b369191 (patch) | |
| tree | 8ee21ee35a2339fa431eb60b3fb04fccaf3f1a64 | |
| parent | a52c53c166c1cc138e2e2189697d126babad1409 (diff) | |
Mini-factorization preparing unification.
| -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 |