| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-13 | Merge PR #11281: [vm] Untabify the VM C code. | Maxime Dénès | |
| Reviewed-by: maximedenes | |||
| 2019-12-12 | Merge PR #11278: Clean libobject stuff | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: maximedenes | |||
| 2019-12-12 | [vm] Untabify the VM C code. | Emilio Jesus Gallego Arias | |
| This is a follow up of #11010 ; I've realized that for example in #11123 a large part of the patch is detabification as indeed the files are mixed in tabs/space style so developers are forced to do the cleanup each time they work on them. Command used: ``` for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` Checked empty diff with `git diff --ignore-all-space` | |||
| 2019-12-12 | Merge PR #11264: Type safe summary & libobject implementation | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-12-12 | Merge PR #11276: Fixing #10750: "Print Visibility" raises Not_found on ↵ | Emilio Jesus Gallego Arias | |
| only-printing notations Ack-by: cpitclaudel Reviewed-by: ejgallego | |||
| 2019-12-11 | Remove the unused add_leaves Libobject primitive. | Pierre-Marie Pédrot | |
| 2019-12-11 | Remove the reliance of ring objects on the named part. | Pierre-Marie Pédrot | |
| This was just dead code. | |||
| 2019-12-11 | Merge PR #11201: remove *.vos and *.vok file in "make clean" | Enrico Tassi | |
| Reviewed-by: gares | |||
| 2019-12-11 | Merge PR #11262: [hashset] Don't use deprecated Obj.truncate | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-12-11 | Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ↵ | Pierre-Marie Pédrot | |
| containing letins. Reviewed-by: ppedrot | |||
| 2019-12-10 | Fixing #10750 (anomaly of "Print Visibility" on only-printing notations). | Hugo Herbelin | |
| 2019-12-10 | Merge PR #10202: Slightly more robust manual implicit arguments | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-12-10 | Merge PR #11269: Several cleanups and factorization in scheme declarations | Emilio Jesus Gallego Arias | |
| Reviewed-by: SkySkimmer Reviewed-by: ejgallego | |||
| 2019-12-10 | Fixing #9893 (Letins not supported in the specialized hypothesis). | Pierre Courtieu | |
| 2019-12-10 | Side-effect free wrapper around already declared schemes. | Pierre-Marie Pédrot | |
| Some calls are actually guarded by a check that the scheme is already in the cache. There is no reason to generate dummy side-effects in that case. | |||
| 2019-12-10 | Make explicit that users should not observe return values of scheme functions. | Pierre-Marie Pédrot | |
| 2019-12-10 | Simplify internal flags in scheme declarations. | Pierre-Marie Pédrot | |
| 2019-12-10 | Merge PR #11268: dune: Add byte mode for coqchk and coqide (fix dune-dbg for ↵ | Emilio Jesus Gallego Arias | |
| dune 2) Reviewed-by: ejgallego | |||
| 2019-12-09 | dune: Add byte mode for coqchk and coqide (fix dune-dbg for dune 2) | Gaëtan Gilbert | |
| dune-dbg depends on coqchk.bc and coqide_main.bc, and apparently they now need explicit modes to be produced. | |||
| 2019-12-09 | Type-safe implementation of libobjects. | Pierre-Marie Pédrot | |
| Same justification as the change in implementation of Summary. | |||
| 2019-12-09 | Simplify the implementation of Summary by specifying the type of ML-MODULES. | Pierre-Marie Pédrot | |
| No need to deploy an existential type machinery when we already know this type in advance. | |||
| 2019-12-09 | Type-safe implementation of summary state. | Pierre-Marie Pédrot | |
| For historical reasons we were wrapping the data stored in the summary objects with dynamic type casts. There is no reason to do so since we have a proper Dyn API. Furthermore, this had a small runtime cost when we knew that it was never going to fail. | |||
| 2019-12-09 | Merge PR #11255: Fix #11254: "coqtop --version" working even in the middle ↵ | Emilio Jesus Gallego Arias | |
| of an installation process Ack-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2019-12-09 | Fixes #11254 (not requiring coqlib to be set to report about coqtop version). | Hugo Herbelin | |
| 2019-12-09 | Merge PR #10829: Section.t is never empty | Pierre-Marie Pédrot | |
| Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-12-09 | Merge PR #11234: [ide] Don't use -linkall for the GUI app. | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-12-09 | [hashset] Don't use deprecated Obj.truncate | Emilio Jesus Gallego Arias | |
| We follow the solution used upstream https://github.com/ocaml/ocaml/pull/2279 Fixes half of #10602 | |||
| 2019-12-09 | Merge PR #11256: [configure] [dune] Fix configure under Dune in 32bit builds. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-12-07 | Section.t is never empty | Gaëtan Gilbert | |
| This approach using `type t = { sec_prev: t option; sec_... }` makes it easy to update sections using the record update syntax, but impossible to statically ensure that an operation only affects the current section. We may instead consider using `type t = section * section list` which needs some boilerplate to update. | |||
| 2019-12-07 | [configure] [dune] Fix configure under Dune in 32bit builds. | Emilio Jesus Gallego Arias | |
| `dev/header.c` is not registered as a dependency, so the configure step under dune fails in 32bit builds. Note we don't detect the problem due to dubious code in configure ignoring stderr messages on process calls. | |||
| 2019-12-07 | Merge PR #11141: Moving the diversity of constr printers to a label style | Emilio Jesus Gallego Arias | |
| Ack-by: SkySkimmer Reviewed-by: ejgallego | |||
| 2019-12-06 | Adding documentation in printer.mli | Hugo Herbelin | |
| 2019-12-06 | Adding overlay for Quickchick PR#145. | Hugo Herbelin | |
| 2019-12-06 | Moving the diversity of constr printers to a label style. | Hugo Herbelin | |
| This allows to give access to all printing options (e.g. a scope or being-in-context) to every printer w/o increasing the numbers of functions. | |||
| 2019-12-06 | Merge PR #11127: Added theorem Nat.bezout_comm. | Hugo Herbelin | |
| Ack-by: Zimmi48 Ack-by: herbelin | |||
| 2019-12-06 | Merge PR #11232: Remove latex files that should be regenerated by make | Théo Zimmermann | |
| Ack-by: Zimmi48 | |||
| 2019-12-06 | Merge PR #11174: [dune] Update to dune language version 2.0 | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-12-05 | Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntax | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2019-12-05 | Merge PR #11172: Interleave removal of coercions and search for notations | Emilio Jesus Gallego Arias | |
| Ack-by: Zimmi48 Reviewed-by: ejgallego | |||
| 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-12-05 | Added Nat.bezout_comm. | Daniel de Rauglaudre | |
| 2019-12-05 | Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tactic | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-12-04 | Manual implicit arguments: more robustness tests. | Hugo Herbelin | |
| - Warn in some places where {x:T} is not assumed to occur (e.g. in argument of an application, or of a match). - Warn when an implicit argument occurs several times with the same name. - Accept local anonymous {_:T} with explicitation possible using name `arg_k`. We obtain this by using a flag (impl_binder_index) which tells if we are in a position where implicit arguments matter and, if yes, the index of the next binder. | |||
| 2019-12-04 | Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident. | Hugo Herbelin | |
| This moves the encoding of "n" as "arg_n" closer to the user interface level. Note however that Constrintern.build_impl is not able yet to use ExplByPos. See further commits. | |||
| 2019-12-04 | Overlay for ELPI | Hugo Herbelin | |
| 2019-12-04 | [dune] Update to dune language version 2.0 | Emilio Jesus Gallego Arias | |
| This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler. | |||
| 2019-12-03 | Update ↵ | Hugo Herbelin | |
| doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 2019-12-03 | Printing: Interleaving search for notations and removal of coercions. | Hugo Herbelin | |
| We renounce to the ad hoc rule preferring a notation w/o delimiter for a term with coercions stripped over a notation for the fully-applied terms with coercions not removed. Instead, we interleave removal of coercions and search for notations: we prefer a notation for the fully applied term, and, if not, try to remove one coercion, and try again a notation for the remaining term, and if not, try to remove the next coercion, etc. Note: the flatten_application could be removed if prim_token were able to apply on a prefix of an application node. | |||
| 2019-12-03 | Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands. | Emilio Jesus Gallego Arias | |
| Reviewed-by: JasonGross Reviewed-by: ejgallego Reviewed-by: maximedenes | |||
| 2019-12-03 | [ide] Don't use -linkall for the GUI app. | Emilio Jesus Gallego Arias | |
| This is incorrect and has created some problems. We also remove unneeded `dynlink` dep. Closes #11217 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |