coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
	Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
2020-10-10	Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵	Hugo Herbelin
	deprecated.
2020-09-11	[parsing] Simplify bigint	Pierre Roux

2020-09-11	[parsing] Rename token NUMERAL to NUMBER	Pierre Roux

2020-05-13	Merge PR #12229: Hopefully consensual cleaning of keywords	Théo Zimmermann
	Reviewed-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2020-05-09	Add a `with_strategy` tactic	Jason Gross
	Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr> Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr> Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
2020-05-06	Stop keeping outdated static list of keywords.	Hugo Herbelin
	The real list is computed by tok_using in CLexer.
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
	Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-22	Adding bignat to parse positive numbers; bigint now includes negative ints.	Hugo Herbelin
	Warning: in notations, the name "bigint" actually meant "bignat". A clarification will eventually be needed.
2020-03-18	Merge PR #11559: Remove year in headers.	Hugo Herbelin
	Reviewed-by: jfehrle
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-03-17	Dead code in g_prim.mlg	Hugo Herbelin

2020-03-03	When parsing negative integer, ensure minus sign is contiguous to the number.	Hugo Herbelin
	For instance, formerly, "Set Inline Level - 1" was succeeding. Now only "Set Inline Level -1" succeeds. (Even though -1 does not make sense for a Inline Level, but that's then a semantic issue. Other options may accept negative numbers in general.)
2020-03-01	Refactor lookaheads using DSL	Maxime Dénès

2020-03-01	Move lookahead combinators to Pcoq	Maxime Dénès
	They were in Ltac2, but they are of general interest
2019-08-06	[parsing] unify checks for contiguity of tokens in Ltac2 and G_prim	Enrico Tassi

2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-05-23	do not parse `\|` as infix in patterns; parse `\|}` as `\|` `}`	Georges Gonthier
	* use mixfix `(p1 \| … \| pn)` notation for nested disjunctive patterns, rather than infix `\|`, making pattern syntax consistent with term syntax. * disable extending `pattern` grammar with notation incompatible with the nested disjunctive pattern syntax `(p1 \| … \| pn)`, such as the `(p \| q)` divisibility notation used by `Numbers`. * emit a (disabled by default) `disj-pattern-notation` warning when such `Notation` is attempted. * update documentation accordingly; document incompatibilities in `changelog`. * comment special treatment of `(num)` in grammar. * update file extensions in `Pcoq` header comment. * correct the keyword declarations to reflect the contents of the grammar files; perhaps there should be an option to disable implicit keyword extension in a `.mlg` file, so that these lists could actually be checked. * parse the `\|}` manifest record terminator as `\|` followed by `}`, eliminating the `\|}` token which conflicts with notations that use `\|` as a terminator (such as, absolute value, norm, or cardinal in MathComp). Since `\|` is now an `operconstr` _and_ `pattern` terminator, `bar_cbrace` rule checks for contiguous symbols, this change entails no visible behaviour change.
2019-04-02	Add parsing of decimal constants (e.g., 1.02e+01)	Pierre Roux
	Rather than integers '[0-9]+', numeral constant can now be parsed according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'. This can be used in one of the two following ways: - using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin - using `Numeral Notation` with the type `decimal` added to `Decimal.v` See examples of each use case in the next two commits.
2019-04-02	Rename the INT token to NUMERAL	Pierre Roux
	In anticipation of future uses of this token for non integer numerals.
2018-11-23	Only use Coq API in coqpp.	Pierre-Marie Pédrot

2018-07-08	Get rid of horrendous hack limiting the size of parsed integers	Maxime Dénès

2018-06-29	Port g_prim to the homebrew GEXTEND parser.	Pierre-Marie Pédrot