| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-07 | [stm] remove tactic_being_run hook | Emilio Jesus Gallego Arias | |
| `tactic_being_run_hook` was used for the "xml" pluging but I am not sure we have a sensible use case here. | |||
| 2017-04-07 | Merge PR#461: [camlpX] Remove camlp4 compat layer. | Maxime Dénès | |
| 2017-04-07 | [toplevel] Remove the feedback feeder printing only on exit. | Emilio Jesus Gallego Arias | |
| This fixes the bug in `Drop` reported by @mattam82: after performing a `Drop`, the feeder was lost and no further message from Coq was printed. | |||
| 2017-04-07 | Fix an unhandled exception in Omega. | Pierre-Marie Pédrot | |
| 2017-04-07 | Better support for printing constructors with let-ins. | Hugo Herbelin | |
| This allows e.g. to use the record notations even when there are defined fields. A priori fixed also missing parameters when interpreting primitive tokens. | |||
| 2017-04-07 | Fixing #4499 (not using unnamed record field in {| |} notation). | Hugo Herbelin | |
| 2017-04-07 | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac) | Matthieu Sozeau | |
| 2017-04-07 | Add some hints to the "real" database to automatically discharge literal ↵ | Guillaume Melquiond | |
| comparisons. | |||
| 2017-04-07 | Merge PR#485: Document Show Match | Maxime Dénès | |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-07 | Remove a forgotten rule for decl_mode from the Makefile. | Pierre-Marie Pédrot | |
| This was making the miniopt target fail. | |||
| 2017-04-07 | Turning the printing primitive projection parameter flag off by default. | Hugo Herbelin | |
| 2017-04-07 | Turning the printing primitive projection compatibility flag off by default. | Hugo Herbelin | |
| 2017-04-07 | [travis] Overlay for PR#461: Camlp4 removal. | Emilio Jesus Gallego Arias | |
| 2017-04-07 | [camlpX] Enrico's changes to camlp4 removal. | Emilio Jesus Gallego Arias | |
| This removes some remaining support for camlp4 in the infrastructure and documents the change. | |||
| 2017-04-07 | [camlpX] Remove camlp4 compat layer. | Emilio Jesus Gallego Arias | |
| We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes. | |||
| 2017-04-07 | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ↵ | Maxime Dénès | |
| printer. | |||
| 2017-04-07 | Merge PR#519: Faster side effects | Maxime Dénès | |
| 2017-04-07 | Inline the only use of hcons_j in Term_typing. | Pierre-Marie Pédrot | |
| 2017-04-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès | |
| 2017-04-06 | Merge PR#488: Adding a documentation for the new proof engine. | Maxime Dénès | |
| 2017-04-06 | Adding a documentation for the new proof engine. | Pierre-Marie Pédrot | |
| 2017-04-06 | Documenting the fact terms are only hashconsed outside of a section. | Pierre-Marie Pédrot | |
| 2017-04-06 | Merge PR#508: Optimize pending evars | Maxime Dénès | |
| 2017-04-06 | Fix a normalization hotspot in computation of constr keys. | Pierre-Marie Pédrot | |
| Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT. | |||
| 2017-04-06 | Factor interp_instance out of Pretyping.pretype_global | Gaetan Gilbert | |
| 2017-04-06 | Avoid strange shadowing of Pretyping.interp_universe_level_name | Gaetan Gilbert | |
| 2017-04-06 | Fix a few programming pearls related to Time, Fail and Redirect. | Maxime Dénès | |
| This fixes a few clear bugs, but the STM code handling Time, Fail and Redirect before par: still needs to be rewritten. It does not implement the same semantics as the vernac interpreter for Fail Fail [c] and ignores Redirect. This commit was already reviewed with Enrico and tested on Travis. | |||
| 2017-04-06 | Merge PR#542: [travis] Add webhook to Gitter. | Maxime Dénès | |
| 2017-04-06 | [travis] Add webhook to Gitter. | Théo Zimmermann | |
| 2017-04-06 | Merge branch 'origin/v8.5' into v8.6. | Hugo Herbelin | |
| Was needed to be done for a while. | |||
| 2017-04-05 | [toplevel] Remove exception error printer in favor of feedback printer. | Emilio Jesus Gallego Arias | |
| We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429 | |||
| 2017-04-05 | Removing a normalization hotspot from EConstr. | Pierre-Marie Pédrot | |
| It was not necessary to normalize a term just to check whether it was a global reference. The hotspot appeared in mathcomp. | |||
| 2017-04-05 | Fixing #5454 (an assert false with 'pat). | Hugo Herbelin | |
| Note: Apparently not easy to make a test file as the error is raised in "G_vernac.fresh_var" at parsing time (not captured by Fail). | |||
| 2017-04-05 | Merge PR#434: Optimizing array mapping in the kernel. | Maxime Dénès | |
| 2017-04-04 | closing bug file for #4306 | Julien Forest | |
| 2017-04-04 | end of correction of bug 4306 | Julien Forest | |
| 2017-04-04 | Bad correction in previous commit | Julien Forest | |
| 2017-04-04 | Solving first problem in bug #4306. TO DO : solve the let in problem | Julien Forest | |
| 2017-04-04 | bug file for 4306 | Julien Forest | |
| 2017-04-04 | Adding tests for chained abstract tactics. | Pierre-Marie Pédrot | |
| 2017-04-04 | Fix substitution of abstracted lemmas. | Pierre-Marie Pédrot | |
| Instead of browsing the term as many times as there are abstracted constants, we replace the constants in one pass. We have to be a bit careful to replace the right variables though, in case there are chained abstracts. This is much faster. This solves the second part of bug #5382: Huge case analysis fails in coq8.5.x. | |||
| 2017-04-04 | Merge PR#502: [pp] Add anomaly header to error messages. | Maxime Dénès | |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-04 | Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly. | Maxime Dénès | |
| 2017-04-04 | Test file for #5435: [Eval native_compute in] raises anomaly. | Maxime Dénès | |
| 2017-04-04 | Fix bug #5435: [Eval native_compute in] raises anomaly. | Maxime Dénès | |
| Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously avoided by a safeguard I put in nativecode.ml. But other kernel changes in this commit should probably be reviewed carefully. | |||
| 2017-04-03 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-03 | Merge PR#533: Instances should obey universe binders even when defined by ↵ | Maxime Dénès | |
| tactics. | |||
| 2017-04-03 | Fix loading of ocamldebug printers. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |