| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-18 | merge-pr: Improve overlay check | Gaëtan Gilbert | |
| 2018-11-18 | Merge PR #9018: [devtools] Small script to setup overlays automatically | Gaëtan Gilbert | |
| 2018-11-17 | Merge PR #8712: [stm] avoid unshare safe env to detect correctly env ↵ | Maxime Dénès | |
| changing tactics | |||
| 2018-11-17 | Merge PR #8992: put protocol/ in ide/.merlin | Pierre-Marie Pédrot | |
| 2018-11-17 | Add an image status for the CI. | Pierre-Marie Pédrot | |
| 2018-11-17 | Merge pull request coq/ltac2#85 from ejgallego/travis | Pierre-Marie Pédrot | |
| [ci] Add travis setup, docker-based. | |||
| 2018-11-17 | Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers. | Pierre-Marie Pédrot | |
| 2018-11-17 | [devtools] Small script to setup overlays automatically | Emilio Jesus Gallego Arias | |
| This is very preliminary but you should get the idea. The script tries to build contribs, then creates a branch and sets the remote properly as to submit a PR. Usage example: ``` ./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi ``` This only works for contributions hosted in github for now. | |||
| 2018-11-17 | [ci] Add travis setup, docker-based. | Emilio Jesus Gallego Arias | |
| Pretty straightforward; need to be enabled in the Travis console tho. | |||
| 2018-11-17 | [vernacextend] Consolidate extension points API | Emilio Jesus Gallego Arias | |
| We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`. | |||
| 2018-11-17 | [coq] Overlay to adapt to coq/coq#9003 | Emilio Jesus Gallego Arias | |
| To be merged when the Coq developers merge the PR upstream. | |||
| 2018-11-17 | [ci] Uniformize casing of makefile targets and ci variables. | Emilio Jesus Gallego Arias | |
| This is convenient as to have better automation. | |||
| 2018-11-17 | [ci] Cleanup of old overlays. | Emilio Jesus Gallego Arias | |
| 2018-11-17 | Merge PR #8968: Miscellaneous CoqIDE fixes | Pierre-Marie Pédrot | |
| 2018-11-17 | [pfedit] Remove cook_proof stub. | Emilio Jesus Gallego Arias | |
| This is barely used and not very useful, clients should use the close_proof API directly. | |||
| 2018-11-17 | [CoqProject] Abstract warning function for CoqProject readers. | Emilio Jesus Gallego Arias | |
| `CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913. | |||
| 2018-11-17 | [ltac] Use CAst nodes in the tactic AST. | Emilio Jesus Gallego Arias | |
| This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR. | |||
| 2018-11-16 | Remove SSR profiling | Jim Fehrle | |
| Deletes the SsrProfiling and SsrMatchingProfiling options | |||
| 2018-11-16 | Merge PR #8779: Remove the implicit tactic feature following #7229. | Matthieu Sozeau | |
| 2018-11-16 | Print logs in appveyor test suite run | Gaëtan Gilbert | |
| It seems we forgot to export when moving the script to a separate file. | |||
| 2018-11-16 | Merge PR #8781: Remove primproj <-> constant dependency in Heads | Pierre-Marie Pédrot | |
| 2018-11-16 | Reimplement Store using Dyn. | whitequark | |
| 2018-11-16 | Add Dyn.anonymous, a more efficient version of Dyn.create (string_of_int n). | whitequark | |
| 2018-11-16 | Use universe names when printing to dot. | Gaëtan Gilbert | |
| 2018-11-16 | Print Universes Subgraph | Gaëtan Gilbert | |
| This adds an optional [Subgraph] part to the Print Universes command, eg [Print Universes Subgraph(i j)] to print only constraints related to i and j (and Prop/Set). | |||
| 2018-11-16 | Make UGraph printing independent of hash order | Gaëtan Gilbert | |
| 2018-11-16 | Print universe names in subtyping error instead of Var(x). | Gaëtan Gilbert | |
| 2018-11-16 | We improve a little bit in printing universe constraints signature mismatch. | Hugo Herbelin | |
| Use of boxes to ensure locality of formatting + use of a prlist_with_sep so that there are breaking points only inbetween the elements and not at the end of the list. | |||
| 2018-11-16 | Print full binders in subtyping incompatible polymorphism error. | Gaëtan Gilbert | |
| Close #8891 | |||
| 2018-11-16 | put protocol/ in ide/.merlin | Gaëtan Gilbert | |
| 2018-11-16 | Add test for Include in -quick mode | Gaëtan Gilbert | |
| 2018-11-16 | Don't redeclare constraints of fields in Include | Gaëtan Gilbert | |
| 2018-11-16 | Termops.iter_constr_with_full_binders = EConstr.iter_with_full_binders | Gaëtan Gilbert | |
| 2018-11-16 | Share open recursor code between econstr and constr | Gaëtan Gilbert | |
| 2018-11-16 | Fix lifting in foo_with_full_binders for (co)fixpoints | Gaëtan Gilbert | |
| 2018-11-16 | Small simplification in fold_constr_with_binders | Gaëtan Gilbert | |
| 2018-11-16 | Remove some univ_flexible_alg from cases | Gaëtan Gilbert | |
| There are a couple left which seem OK. | |||
| 2018-11-16 | No Projection.constant in projection <-> constant declaration | Gaëtan Gilbert | |
| Enabled by previous commit about Heads. | |||
| 2018-11-16 | Heads: simplify using that projections are always rigid | Gaëtan Gilbert | |
| This avoids using Projection.constant in kind_of_head, which then allows compute_head to not check whether the constant is a compatibility definition (as in that case its body is [fun ... => x.(p)]). Thus Heads stops caring about the compatibility projection system. | |||
| 2018-11-16 | Do not Export the init modules | Gaëtan Gilbert | |
| It seems we started doing the export silently in 47804492bd09c8b13b5aac45800d067dbdf04d00. | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-16 | Merge PR #8888: Proof runcountable rebase | Hugo Herbelin | |
| 2018-11-15 | Merge PR #8991: coqide: use correct toplevel name in files | Emilio Jesus Gallego Arias | |
| 2018-11-15 | Move generating library dirpath to stm in compile mode. | Gaëtan Gilbert | |
| 2018-11-15 | coqide: use correct toplevel name in files | Gaëtan Gilbert | |
| Fix #8989. This adds an option -topfile taking a path so that inferring the right dirpath is done by the toplevel after processing -Q/-R instead of the client having to do it. | |||
| 2018-11-15 | Make set_typing_flags "smart" | Gaëtan Gilbert | |
| Fix #8609 gares said: I believe it was introduced in de20a45 where the option (part of the summary) is moved to the save env. By setting the summary, you unshare the safe env. Now we do that only if needed. The stm uses `==` on the safe env to detect tactics that alter the env, eg abstract. | |||
| 2018-11-15 | Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p" | Vincent Laporte | |
| 2018-11-15 | Fix compilation w.r.t. coq/coq#8779. | Pierre-Marie Pédrot | |
| 2018-11-14 | Get hyps and goal the same way Printer does; don't omit info | Jim Fehrle | |
| Allow for new goals that don't map to old goals Include background_goals in all_goals return value Fix incorrect change to raw diffs in shorten_diff_span Fixes #8922 | |||
| 2018-11-14 | Merge PR #8966: coq_makefile: Fix ocamldep ignoring mlg files | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |