| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-08 | Fix Typo in Doc for `Set Parsing Explicit` | staffehn | |
| 2017-09-08 | Normalizing universes before performing term comparison. | Pierre-Marie Pédrot | |
| This code was probably slightly wrong w.r.t. to a semantics defined as equivalent to first full-blown normalization followed by kernel term equality. Or at least, it was adding redundant constraints. | |||
| 2017-09-08 | Using EConstr equality check in unification. | Pierre-Marie Pédrot | |
| The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr. | |||
| 2017-09-08 | Using a dedicated argument for tactic quotations. | Pierre-Marie Pédrot | |
| This prevents having to go through an expensive phase of goal-building, when we can simply type-check the term. | |||
| 2017-09-08 | Fix the introduction of SSR refman chapter. | Théo Zimmermann | |
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | |
| When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family. | |||
| 2017-09-08 | Move README.ci and link to it from CONTRIBUTING. | Théo Zimmermann | |
| 2017-09-08 | Update CI policy. | Théo Zimmermann | |
| 2017-09-08 | Fix coq/ltac2#27: ... is not a particularly helpful printing of an error ↵ | Pierre-Marie Pédrot | |
| message. | |||
| 2017-09-08 | Fix coq/ltac2#24: There should be a way to turn an exn into a message. | Pierre-Marie Pédrot | |
| 2017-09-08 | Fix coq/ltac2#22: Argument to Tactic_failure should be printed. | Pierre-Marie Pédrot | |
| We implement a printer for toplevel values and use it for exceptions in particular. | |||
| 2017-09-07 | Slightly better printing for anonymous closures. | Pierre-Marie Pédrot | |
| 2017-09-07 | Fix coq/ltac2#21: Backtraces should print Ltac2 closures. | Pierre-Marie Pédrot | |
| 2017-09-07 | Merge PR #997: coqdoc: Support comments in verbatim output | Maxime Dénès | |
| 2017-09-07 | Fix BZ#5655 by avoiding the creation of a cleaner thread for empty queues. | Maxime Dénès | |
| While this is a good workaround, Enrico has a minimal example of the underlying issue that we will send to the OCaml team. | |||
| 2017-09-07 | Merge PR #1016: 2 Typos in 'Add Parametric Morphism' Documentation | Maxime Dénès | |
| 2017-09-07 | Merge PR #968: Better error messages on the CI | Maxime Dénès | |
| 2017-09-07 | dev/build/windows/makecoq_mingw.sh: install camlp5's META file | Enrico Tassi | |
| 2017-09-07 | Merge PR #931: Parametrize module body | Maxime Dénès | |
| 2017-09-07 | Merge PR #914: Making the detyper lazy | Maxime Dénès | |
| 2017-09-07 | Merge PR #904: Add build_coq_or to API.Coqlib | Maxime Dénès | |
| 2017-09-07 | Trying to properly propagate errors in Windows CI script. | Maxime Dénès | |
| 2017-09-07 | Communicate the backtrace through the monad. | Pierre-Marie Pédrot | |
| 2017-09-06 | Fix coq/ltac2#23: Int.compare should not be uniformly 0. | Pierre-Marie Pédrot | |
| Stupid typo. | |||
| 2017-09-06 | Using higher-order representation for closures. | Pierre-Marie Pédrot | |
| 2017-09-06 | Parameterizing over parameters in ML functions from Tac2core. | Pierre-Marie Pédrot | |
| 2017-09-06 | The interp_app function now takes a closure as an argument. | Pierre-Marie Pédrot | |
| 2017-09-06 | Moving Tac2ffi before Tac2interp. | Pierre-Marie Pédrot | |
| 2017-09-06 | Introducing abstract data representations. | Pierre-Marie Pédrot | |
| 2017-09-06 | use get_arguments, String.concat, remove -I | Paul Steckler | |
| 2017-09-06 | Fix a refine anomaly "Evar defined twice". | Pierre-Marie Pédrot | |
| Because the argument given to refine may mess with the evarmap, the goal being refined can be solved by side-effect after the term filler is computed. If this happens, we simply don't perform the refining operation. | |||
| 2017-09-06 | Code factorization. | Pierre-Marie Pédrot | |
| 2017-09-06 | weakens an hypothesis of Rle_Rpower | Yves Bertot | |
| 2017-09-06 | changed statements of Rpower_lt and Rle_power and added | Yves Bertot | |
| Rlt_Rpower_l and pow_INR. Unfortunately theorems Rpower_lt and Rle_power are named inconsistently, in spite of their similarity. | |||
| 2017-09-06 | Merge PR #1022: Appveyor package | Maxime Dénès | |
| 2017-09-05 | read flags from project file for Compile Buffer | Paul Steckler | |
| 2017-09-05 | Refine does not evar-normalizes the goal preemptively. | Pierre-Marie Pédrot | |
| 2017-09-05 | Make AppVeyor generate Windows package. | Maxime Dénès | |
| 2017-09-05 | Binding the firstorder tactic. | Pierre-Marie Pédrot | |
| 2017-09-05 | Remove -debug option from Windows build script. | Maxime Dénès | |
| It is no longer accepted by Coq's ./configure. | |||
| 2017-09-05 | Get sources of cygwin packages after building the installer. | Maxime Dénès | |
| 2017-09-05 | Adapt Windows build script to new CoqIDE data installation directory. | Maxime Dénès | |
| 2017-09-05 | Print more of the Coq build output. | Maxime Dénès | |
| 2017-09-05 | Print Coq build output. | Maxime Dénès | |
| 2017-09-05 | In regression test mode, run cygwin setup to install dependencies. | Maxime Dénès | |
| 2017-09-05 | Export Ltac2.Notations in the Ltac2 entry module. | Pierre-Marie Pédrot | |
| 2017-09-05 | The absurd tactic now parses a constr. | Pierre-Marie Pédrot | |
| 2017-09-05 | Binding move and intro. | Pierre-Marie Pédrot | |
| 2017-09-05 | Merge PR #1011: fix test-suite/coq-makefile/findlib-package on windows after ↵ | Maxime Dénès | |
| #958 | |||
| 2017-09-05 | Introducing quotations for move locations. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |