diff options
| author | Gaëtan Gilbert | 2018-02-20 15:35:25 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-05 14:21:47 +0100 |
| commit | 88f3b5a441a3aaeb637d0b109544fbe71b7560dd (patch) | |
| tree | ddbe8c3c4e1e2d773078254b0cef162126503709 /vernac/comFixpoint.ml | |
| parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) | |
Allow universe declarations for [with Definition].
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index edfe7aa819..a794c2db06 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -14,7 +14,6 @@ open Pretyping open Evarutil open Evarconv open Misctypes -open Vernacexpr module RelDecl = Context.Rel.Declaration |