From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Jun 2017 15:12:21 +0200 Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof` `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. --- parsing/g_vernac.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'parsing') diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index dbd2fc401..fe8f517a7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -151,7 +151,7 @@ GEXTEND Gram l = LIST0 [ "with"; id = pidentref; bl = binders; ":"; c = lconstr -> (Some id,(bl,c)) ] -> - VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false) + VernacStartTheoremProof (thm, (Some id,(bl,c))::l) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> -- cgit v1.2.3