| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-23 | Relying on the abstract notion of streams with location for parsing. | Hugo Herbelin | |
| We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml). | |||
| 2021-01-02 | Deprecate "at ... with ..." in change tactic | Jim Fehrle | |
| (use "with ... at ..." instead) | |||
| 2020-11-23 | Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵ | coqbot-app[bot] | |
| sense Reviewed-by: Zimmi48 | |||
| 2020-11-21 | Merge PR #12246: Adding support for applying in several hypotheses at the ↵ | Pierre-Marie Pédrot | |
| same time (granting #9816) Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2020-11-20 | Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clauses | Pierre-Marie Pédrot | |
| Reviewed-by: jfehrle Reviewed-by: ppedrot | |||
| 2020-11-20 | Use nat_or_var where negative values don't make sense | Jim Fehrle | |
| 2020-11-20 | Granting #9816: apply in takes several hypotheses. | Hugo Herbelin | |
| 2020-11-18 | Use only nats for occs_nums rather than ints | Jim Fehrle | |
| 2020-11-17 | Fixes #13235: remove fragile tolerance for degenerate in-hyps clause. | Hugo Herbelin | |
| Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2020-11-16 | Suggesting to use injection when an injection pattern is given to destruct. | Hugo Herbelin | |
| This hopefully clarifies the confusing role of destruct (see #13205). | |||
| 2020-10-30 | Renaming Numeral into Number | Pierre Roux | |
| 2020-10-27 | Rename misc nonterminals | Jim Fehrle | |
| 2020-10-27 | Rename tactic_expr -> ltac_expr | Jim Fehrle | |
| 2020-10-27 | Rename operconstr -> term | Jim Fehrle | |
| 2020-10-10 | Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵ | Hugo Herbelin | |
| deprecated. | |||
| 2020-05-06 | Stop keeping outdated static list of keywords. | Hugo Herbelin | |
| The real list is computed by tok_using in CLexer. | |||
| 2020-03-26 | Removing deprecated destruct syntax _eqn. | Hugo Herbelin | |
| 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-18 | Update headers in the whole code base. | Théo Zimmermann | |
| Add headers to a few files which were missing them. | |||
| 2020-03-05 | Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ↵ | Pierre-Marie Pédrot | |
| following the model of `pose (x:=t)`. Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2020-03-03 | Adding an alias "pose proof (x:=a)" for "pose proof a as x". | Hugo Herbelin | |
| This is to be consistent with "pose (x:=a)" (and an alternative to "assert (x:=a)"). This was suggested by "https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962". | |||
| 2020-03-01 | [parser] lk_int -> lk_nat | Maxime Dénès | |
| 2020-03-01 | Refactor lookaheads using DSL | Maxime Dénès | |
| 2019-12-05 | Unfortunate bug with "cofix with": case of a CProdN over no bindings. | Hugo Herbelin | |
| Failing on CProdN([],...) was maybe a bit too radical. | |||
| 2019-11-21 | [coq] Untabify the whole ML codebase. | Emilio Jesus Gallego Arias | |
| We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` | |||
| 2019-11-14 | Rename non-unique local nonterminals | Jim Fehrle | |
| 2019-10-18 | factorize or_var_map | Alexandre Moine | |
| 2019-08-19 | [api] Move handling of variable implicit data to impargs | Emilio Jesus Gallego Arias | |
| We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function. | |||
| 2019-07-29 | Tentatively providing a localization function to ad-hoc camlp5 parsers. | Pierre-Marie Pédrot | |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2019-04-29 | Exposing a change_no_check tactic. | Hugo Herbelin | |
| 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. | |||
| 2019-04-01 | Replace type sign = bool with SPlus | SMinus | Pierre Roux | |
| 2019-01-23 | Move and rewrite documentation for intro patterns that was under | Jim Fehrle | |
| the intros tactic to its own subsection. Add grammar and examples. | |||
| 2018-11-23 | Remove the unsafe camlp5 API from the Coq codebase. | Pierre-Marie Pédrot | |
| 2018-11-17 | [ltac] Use CAst nodes in the tactic AST. | Emilio Jesus Gallego Arias | |
| This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR. | |||
| 2018-09-23 | [api] Deprecate constructors of deprecated datatypes. | Emilio Jesus Gallego Arias | |
| When deprecating some type alias [due to code refactoring] we forgot to deprecate the constructors too. Closes #8498. | |||
| 2018-06-29 | Port g_tactic to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |