From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Apr 2017 11:21:23 +0200 Subject: 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. --- ide/texmacspp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide/texmacspp.ml') 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]) -- cgit v1.2.3