diff options
| author | Emilio Jesus Gallego Arias | 2019-06-22 02:37:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-09 12:42:03 +0200 |
| commit | 515e7039857d85f7c6eec9272e0ca3b45162d978 (patch) | |
| tree | 6723753bf51c949c0729e8fcec94451df0a2e099 /vernac/declareObl.ml | |
| parent | 7f366a7c7cd154c6a1dd191ff7f453e63b39a948 (diff) | |
[proof] Remove sign parameter to open_lemma.
The current code does some "opacification" for `Let`s, however that's
pretty fragile in general and not all codepaths do respect it.
We need to decide what to do.
Diffstat (limited to 'vernac/declareObl.ml')
| -rw-r--r-- | vernac/declareObl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index c7b8b13282..0c45ff11d7 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -53,7 +53,7 @@ type program_info = ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool - ; prg_sign : named_context_val } + } (* Saving an obligation *) |