| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-29 | Remove outdated patch from ci-sf | Jasper Hugunin | |
| 2018-03-10 | [ssreflect] Fix module scoping problems due to packing and mli files. | Emilio Jesus Gallego Arias | |
| Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512. | |||
| 2018-03-09 | [located] Push inner locations in `reference` to a CAst.t node. | Emilio Jesus Gallego Arias | |
| The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now. | |||
| 2018-03-09 | [located] More work towards using CAst.t | Emilio Jesus Gallego Arias | |
| We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes. | |||
| 2018-03-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 2018-03-09 | Overlay for Elpi. | Gaëtan Gilbert | |
| 2018-03-09 | Add an overlay for Equations and Ltac2. | Pierre-Marie Pédrot | |
| 2018-03-08 | Merge PR #6881: [windows] support -addon in build script | Maxime Dénès | |
| 2018-03-06 | build: win: turn off build/installation of gnu Make | Enrico Tassi | |
| 2018-03-04 | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`. | Maxime Dénès | |
| 2018-03-04 | Merge PR #6676: [proofview] goals come with a state | Maxime Dénès | |
| 2018-03-02 | build: win: addon bignums | Enrico Tassi | |
| 2018-02-28 | [econstr] Continue consolidation of EConstr API under `interp`. | Emilio Jesus Gallego Arias | |
| This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag. | |||
| 2018-02-22 | [ast] Improve precision of Ast location recognition in serialization. | Emilio Jesus Gallego Arias | |
| We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way. | |||
| 2018-02-20 | overlay for ltac2 and Equations | Enrico Tassi | |
| 2018-02-19 | ci: add elpi | Enrico Tassi | |
| 2018-02-12 | Merge PR #6706: ci-common: guess CI_BRANCH for local builds | Maxime Dénès | |
| 2018-02-07 | Merge PR #6610: Points to Flocq official repository. | Maxime Dénès | |
| 2018-02-07 | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | Maxime Dénès | |
| 2018-02-07 | ci-common: guess CI_BRANCH for local builds | Gaëtan Gilbert | |
| 2018-02-05 | Points to Flocq official repository. | Théo Zimmermann | |
| Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528. | |||
| 2018-02-05 | Add overlay for equations (nf_beta takes an env) | Gaëtan Gilbert | |
| 2018-02-05 | Merge PR #6654: CI: Run coqchk on Iris | Maxime Dénès | |
| 2018-01-31 | CI: Run coqchk on Iris | Ralf Jung | |
| 2018-01-31 | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵ | Maxime Dénès | |
| menhir. | |||
| 2018-01-31 | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | |
| 2018-01-30 | Put default value for NJOBS in ci-common. | Gaëtan Gilbert | |
| 2018-01-30 | Adding an overlay for Equations. | Pierre-Marie Pédrot | |
| 2018-01-23 | Merge PR #6568: Cleanup scripts | Maxime Dénès | |
| 2018-01-16 | Source basic overlay before user overlays. | Gaëtan Gilbert | |
| 2018-01-16 | Cleanup shell expansions and quoting. | Gaëtan Gilbert | |
| 2018-01-12 | Merge PR #6483: Strong invariants in polymorphic definitions | Maxime Dénès | |
| 2018-01-11 | Adding a custom Travis overlay for HoTT. | Pierre-Marie Pédrot | |
| 2018-01-11 | Merge PR #6557: First stab at documenting the test suite. | Maxime Dénès | |
| 2018-01-06 | First stab at documenting the test suite. | Jasper Hugunin | |
| 2018-01-04 | Normalize Windows installer names. | Théo Zimmermann | |
| 2017-12-29 | Merge PR #6493: [API] remove large file containing duplicate interfaces | Maxime Dénès | |
| 2017-12-29 | Merge PR #6405: Remove the local polymorphic flag hack. | Maxime Dénès | |
| 2017-12-27 | overlay for #6493 | Enrico Tassi | |
| 2017-12-27 | Merge PR #6102: Fix #5998: AppVeyor package building is currently failing | Maxime Dénès | |
| 2017-12-27 | Add equations overlay. | Maxime Dénès | |
| 2017-12-27 | Fix #5998: AppVeyor package building is currently failing | Maxime Dénès | |
| 2017-12-26 | Fix overlay selection for Circle CI. | Gaëtan Gilbert | |
| 2017-12-26 | Delete old overlays (leaving example) | Gaëtan Gilbert | |
| 2017-12-21 | Fix CI with parallel make (messed up dependencies) | Gaëtan Gilbert | |
| When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper. | |||
| 2017-12-19 | Merge PR #6400: Circle CI | Maxime Dénès | |
| 2017-12-18 | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | |
| 2017-12-18 | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | Maxime Dénès | |
| 2017-12-15 | Overlay for unimath. | Gaëtan Gilbert | |
| 2017-12-15 | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml` | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |