| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-14 | Adding missing newline in coqc usage. | Hugo Herbelin | |
| 2019-05-14 | CoqIDE: Treat unknown arguments starting with dash as unknown options rather ↵ | Hugo Herbelin | |
| than files. | |||
| 2019-05-14 | Removing no more existing option -emacs-U. | Hugo Herbelin | |
| 2019-05-14 | Usage: fixing indentation for set/unset options. | Hugo Herbelin | |
| 2019-05-14 | Ensuring suffix of file to compile also for -vio2vo checking. | Hugo Herbelin | |
| We do it by consistently using variants of the "ensure_exists" policy in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and parallel vio checking (schedule-vio-checking). For instance, coqc -vio2vo dir/file.vio now works, while before, dir/file was expected. Incidentally, this avoids the non-recommended Loadpath.locate_file. | |||
| 2019-05-14 | Option -check-vio-tasks: fail gracefully when not finding expected integers. | Hugo Herbelin | |
| 2019-05-14 | Merge PR #10152: Move last changelog entries for 8.10+beta1. | Vincent Laporte | |
| Reviewed-by: vbgl | |||
| 2019-05-13 | Handle tags shorter than "diff." without an exception | Jim Fehrle | |
| 2019-05-13 | Adding overlay for Equations. | Hugo Herbelin | |
| 2019-05-13 | Passing evar_map to evars_of_term rather than expecting the term to be evar-nf. | Hugo Herbelin | |
| 2019-05-13 | Moving Evd.evars_of_term from constr to econstr + consequences. | Hugo Herbelin | |
| This impacts a lot of code, apparently in the good, removing several conversions back and forth constr. | |||
| 2019-05-13 | Missing change entry for #9854. | Théo Zimmermann | |
| 2019-05-13 | Move last changelog entries for 8.10+beta1. | Théo Zimmermann | |
| 2019-05-13 | Merge PR #10085: Do not include unreleased changelog in released versions. | Vincent Laporte | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: jfehrle Reviewed-by: vbgl | |||
| 2019-05-13 | Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵ | Enrico Tassi | |
| prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl | |||
| 2019-05-13 | Merge PR #9887: [api] Remove 8.10 deprecations. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-13 | Add overlay for Unicoq | Maxime Dénès | |
| 2019-05-13 | Make detyping robust w.r.t. indexed anonymous variables | Maxime Dénès | |
| I don't think there's a reason to treat such variables more severely than unbound variables. This anomaly is often raised by debug printers (e.g. when studying complex scenarios using `Set Unification Debug`), and so makes debugging less convenient. Fixes #3754, fixes #10026. | |||
| 2019-05-13 | Merge PR #10061: Print custom grammar entries | Vincent Laporte | |
| Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: jashug | |||
| 2019-05-13 | Merge PR #10079: [refman] Move Ltac examples to Ltac chapter. | Vincent Laporte | |
| Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot | |||
| 2019-05-12 | [refman] Raise an error when a notation doesn't parse | Clément Pit-Claudel | |
| 2019-05-12 | [refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug' | Clément Pit-Claudel | |
| 2019-05-12 | Merge PR #10083: Avoid trivial (u=u) constraints in AcyclicGraph.constraints_for | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-05-11 | Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS ↵ | Pierre-Marie Pédrot | |
| + adding a go-to-end binding + improving documentation Reviewed-by: gares Ack-by: herbelin Reviewed-by: ppedrot | |||
| 2019-05-11 | Remove the sidecond_first flag of apply-related tactics. | Pierre-Marie Pédrot | |
| This was dead code. | |||
| 2019-05-11 | Remove the elimrename field from Tactics.eliminator. | Pierre-Marie Pédrot | |
| This is actually dead code, we never observe it. | |||
| 2019-05-11 | Code factorization in elim tactics. | Pierre-Marie Pédrot | |
| This is just moving code around, so it should not change the semantics. | |||
| 2019-05-11 | Actually use the conversion locality flag. | Pierre-Marie Pédrot | |
| Fixes #9919. | |||
| 2019-05-11 | Introducing a local flag to hypothesis conversion function. | Pierre-Marie Pédrot | |
| If the reduction function is known not to depend on the named context, then we can perform it in parallel on the various variables. | |||
| 2019-05-11 | Generalize map_named_val to handle whole declarations. | Pierre-Marie Pédrot | |
| 2019-05-11 | Abstract the Tactic.e_change_hyps function over the reduction function. | Pierre-Marie Pédrot | |
| 2019-05-11 | Merge PR #10052: Cleanup the hypothesis conversion function | Hugo Herbelin | |
| Reviewed-by: herbelin | |||
| 2019-05-10 | Use Print Custom Grammar to inspect custom entries | Jasper Hugunin | |
| 2019-05-10 | [refman] Mention the `#[canonical(false)]` attribute | Vincent Laporte | |
| 2019-05-10 | [Attributes] Allow explicit value for two-valued attributes | Vincent Laporte | |
| Attributes that enable/disable a feature can have an explicit value (default is enable when the attribute is present). Three-valued boolean attributes do not support this: what would `#[local(false)]` mean? | |||
| 2019-05-10 | Add overlay for elpi | Vincent Laporte | |
| 2019-05-10 | Changelog for PR #10076 | Vincent Laporte | |
| 2019-05-10 | [User manual] Fix two warnings related to canonical structures | Vincent Laporte | |
| 2019-05-10 | [Canonical structures] “not_canonical” annotation to field declarations | Vincent Laporte | |
| 2019-05-10 | [Canonical structures] Some projections may not be canonical | Vincent Laporte | |
| 2019-05-10 | Merge PR #10058: Remove various circumvolutions from reduction behaviors | Enrico Tassi | |
| Ack-by: SkySkimmer Reviewed-by: gares Ack-by: maximedenes | |||
| 2019-05-10 | Merge PR #10080: Define minimum Sphinx version in conf.py. | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel Reviewed-by: vbgl | |||
| 2019-05-10 | [ltac2] Add primitive integers | Pierre Roux | |
| 2019-05-10 | Merge PR #9854: Improve field_simplify on fractions with constant denominator | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: amahboubi Reviewed-by: vbgl | |||
| 2019-05-10 | Merge PR #10065: CI: run coqchk without -silent | Emilio Jesus Gallego Arias | |
| 2019-05-10 | Add overlays for coq/coq#10052. | Pierre-Marie Pédrot | |
| 2019-05-10 | Fast-path for reordering of a single closed variable. | Pierre-Marie Pédrot | |
| Doesn't seem to matter in practice, but it doesn't hurt either. | |||
| 2019-05-10 | Take advantage of the ordering / conversion check split. | Pierre-Marie Pédrot | |
| 2019-05-10 | Split the hypothesis conversion check in a conversion + ordering check. | Pierre-Marie Pédrot | |
| 2019-05-10 | Make the check flag of conversion functions mandatory. | Pierre-Marie Pédrot | |
| The current situation is a mess, some functions set it by default, but other no. Making it mandatory ensures that the expected value is the correct one. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |