diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-02 11:21:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-09 11:52:17 +0200 |
| commit | 1a43fda0dc9bb8d100808426980446353f8f1ae3 (patch) | |
| tree | 5907412903414e3c21d718a70dc0d377a3589b1a /ide | |
| parent | 2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff) | |
Removing internal support for accepting "{struct x}" and co in "Theorem with".
There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/texmacspp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index e787e48bf..74d0438dd 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -553,7 +553,7 @@ let rec tmpp v loc = let str_dk = Kindops.string_of_definition_kind (l, false, dk) in let str_id = Id.to_string id in (xmlDef str_dk str_id loc [pp_expr e]) - | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> + | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement) ], b) -> let str_tk = Kindops.string_of_theorem_kind tk in let str_id = Id.to_string id in (xmlThm str_tk str_id loc [pp_expr statement]) |