| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-11-14 | ssr: add another test for elim + TC | Enrico Tassi | |
| 2018-11-14 | ssr: rewrite: do resolve TC once and forall at the very end | Enrico Tassi | |
| 2018-11-14 | ssr: elim: do resolve TC once and forall at the very end | Enrico Tassi | |
| 2018-11-14 | ssrcommon: API to call resolve_tyclasses on a term | Enrico Tassi | |
| 2018-11-14 | ssrmatching: unify_HO does not resolve type classes | Enrico Tassi | |
| 2018-11-14 | [mailmap] Update "anonymous" accounts. | Théo Zimmermann | |
| Of the three "anonymous" accounts, one ("coq") was used by multiple authors (in particular Jacek Chrząszcz who developed the module system), while the other two are each the committer of a single auto-generated commit so we rename them to cvs2svn and serpyc-bot. | |||
| 2018-11-14 | Update .mailmap. | Théo Zimmermann | |
| 2018-11-14 | Deprecate hint declaration/removal with no specified database | Maxime Dénès | |
| Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach). | |||
| 2018-11-13 | Merge PR #8886: [VM] Fix compilation of int31 eliminators | Maxime Dénès | |
| 2018-11-13 | Merge PR #8906: [Goptions] More detailed error messages | Maxime Dénès | |
| 2018-11-13 | Merge PR #8760: Automatically generate names for universes. | Pierre-Marie Pédrot | |
| 2018-11-13 | coq_makefile: Fix ocamldep ignoring mlg files | Gaëtan Gilbert | |
| If you have file1.mlg and file2.ml, with file2 depending on file1, ocamldep was before generating file1.ml so wouldn't generate [file2.cmx: file1.cmx] (ocamldep is silent on non-found dependencies). This has been causing nondeterministic failures in quickchick recently. I guess it didn't come up in the past because ml4 files tend to be at the end of the dependency chain. | |||
| 2018-11-13 | Merge PR #8976: CoqHammer CI | Gaëtan Gilbert | |
| 2018-11-13 | Merge PR #8957: Fix -top for univbinders output test. | Emilio Jesus Gallego Arias | |
| 2018-11-13 | Port to coqpp. | Pierre-Marie Pédrot | |
| 2018-11-13 | Merge PR #8919: [vernac] Rename Vernacinterp to Vernacextend and move ↵ | Pierre-Marie Pédrot | |
| extension functions there | |||
| 2018-11-13 | [vernac] Rename Vernacinterp to Vernacextend and move extension functions there. | Emilio Jesus Gallego Arias | |
| This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |