diff options
Diffstat (limited to 'vernac/g_proofs.mlg')
| -rw-r--r-- | vernac/g_proofs.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 80a4de472c..ebec720ce2 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -64,12 +64,12 @@ GRAMMAR EXTEND Gram | IDENT "Existential"; n = natural; c = constr_body -> { VernacSolveExistential (n,c) } | IDENT "Admitted" -> { VernacEndProof Admitted } - | IDENT "Qed" -> { VernacEndProof (Proved (Declare.Opaque,None)) } + | IDENT "Qed" -> { VernacEndProof (Proved (Opaque,None)) } | IDENT "Save"; id = identref -> - { VernacEndProof (Proved (Declare.Opaque, Some id)) } - | IDENT "Defined" -> { VernacEndProof (Proved (Declare.Transparent,None)) } + { VernacEndProof (Proved (Opaque, Some id)) } + | IDENT "Defined" -> { VernacEndProof (Proved (Transparent,None)) } | IDENT "Defined"; id=identref -> - { VernacEndProof (Proved (Declare.Transparent,Some id)) } + { VernacEndProof (Proved (Transparent,Some id)) } | IDENT "Restart" -> { VernacRestart } | IDENT "Undo" -> { VernacUndo 1 } | IDENT "Undo"; n = natural -> { VernacUndo n } |