| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-15 | Bug 3628 is fixed. | Matthieu Sozeau | |
| 2014-10-15 | Fix test-suite files which failed due to usage of $(admit)$ which | Matthieu Sozeau | |
| now fails with Error: Already an existential evar of name Main | |||
| 2014-10-15 | Fix bug 3637. | Matthieu Sozeau | |
| 2014-10-15 | Reenable FO unification of primitive projections and their eta-expanded | Matthieu Sozeau | |
| forms in evarconv and unification, as well as fallback to first-order unification when eta for constructors fail. Update test-suite file 3484 to test for the FO case in evarconv as well. | |||
| 2014-10-15 | Fix test-suite file after moving back to using C as the name | Matthieu Sozeau | |
| of the record binder for Class C's projections. | |||
| 2014-10-15 | Modify the heuristic for unfolding lhs or rhs in evarconv, considering | Matthieu Sozeau | |
| folded primitive projections in applicative stacks in rhs as named, hence prefering to unfold the lhs in these cases. | |||
| 2014-10-15 | Implement a different strategy to expand primitive projections only when | Matthieu Sozeau | |
| required, i.e. in first-order unification cases where the head of the other side is a hole or the eta-expanded constant. | |||
| 2014-10-15 | Add an option to not print primitive projection parameters, which can | Matthieu Sozeau | |
| make printing exponentially slower. We would have to expand all projections at once before detyping to make this linear. | |||
| 2014-10-15 | Fix -async-proofs-always-delegate (close 3740) | Enrico Tassi | |
| 2014-10-14 | Fix ML paths (thanks Jean-Marc Notin for bisecting it) | Enrico Tassi | |
| 2014-10-14 | Revert "Move eta-expansion after delta reduction in kernel reduction. This ↵ | Matthieu Sozeau | |
| makes" This makes CatsInZFC explode by expanding constants unnecessarily. This reverts commit cf36105854c9a42960ee4139c6afdaa75ec8f31a. | |||
| 2014-10-14 | Oops, forgot a fix needed after the rebase. | Matthieu Sozeau | |
| 2014-10-14 | Fix bug #3698: stack overflow due to eta+canonical structures in | Matthieu Sozeau | |
| unification. | |||
| 2014-10-13 | Fix typo, thanks Mike Shulman for spotting it | Enrico Tassi | |
| 2014-10-13 | Fixing "change" and "fold" after convert_hyp/convert_concl moved to | Hugo Herbelin | |
| new proof engine in e824d4293. Because of the expansion made by "fold" and possibly by "change", checking the order of hypotheses is necessary in general in "reduce". Before, it was done by side-effect on reference "check", now it has to be explicit. To do for optimization: flag each of the red_expr conversion strategy according to whether they really need a check. Also renamed the e_reduce family to e_change to emphasize that some expansion can occur and that typing has to be rechecked. This fixes recent failure of CoLoR (and probably Ergo). | |||
| 2014-10-13 | Add support for deactivating type class inference from induction/destruct. | Hugo Herbelin | |
| 2014-10-13 | Adding a tactic which fails if one of the goals under focus is dependent in ↵ | Hugo Herbelin | |
| another one. | |||
| 2014-10-13 | Adding printers for ppproofview. | Hugo Herbelin | |
| 2014-10-13 | Naming main goal "Main" | Hugo Herbelin | |
| 2014-10-13 | Moving function about locs in locusops. | Hugo Herbelin | |
| 2014-10-13 | English typo in a function name of evarconv. | Hugo Herbelin | |
| 2014-10-13 | Added support for several impossible cases in compilation of "match". | Hugo Herbelin | |
| 2014-10-13 | Stm: more precise representation of nested proofs | Enrico Tassi | |
| This fixes the bug reported by Hugo: 2) Goal True. 3-4) Definition a:=0. 5) Goal True True. (* jumped back to 3 (on master) instead of 4 (on the outermost proof) *) | |||
| 2014-10-13 | When loading libraries, feed back dependencies. | Carst Tankink | |
| These dependencies between files can be used by UIs to guide compilation and reloading of files. FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar. FileDependency (None, "/bar.v") means the current file depends on bar. | |||
| 2014-10-13 | Emit a warning for void Arguments statement (Close 3713) | Enrico Tassi | |
| 2014-10-13 | Parsing of "?[" as two tokens (makes ssr compile). | Enrico Tassi | |
| The problem is that "?[" makes the lexer glue "?" and "[" into a single token but in ssr "?" (iteration) and "[" (rewrite pattern delimiter) are often close, but they are parsed by very hard to refactor grammar entries. To consider: - check the adjacency of the two symbols looking at the loc to parse exactly the same sentences as before this patch - change syntax completely, e.g. "(_ as id)" | |||
| 2014-10-13 | STM: primitives to snapshot a .vi while in interactive mode | Enrico Tassi | |
| 2014-10-13 | selective join/export of the safe_environment | Enrico Tassi | |
| This generalizes the BuildVi flag and lets one choose which opaque proofs are done and which not. | |||
| 2014-10-13 | TQueue: new primitive to take a snapshot of the queue | Enrico Tassi | |
| 2014-10-13 | STM: simplify how the term part of a side effect is retrieved | Enrico Tassi | |
| Now the seff contains it directly, no need to force the future or to hope that it is a Direct opaque proof. | |||
| 2014-10-13 | library/opaqueTables: enable their use in interactive mode | Enrico Tassi | |
| Before this patch opaque tables were only growing, making them unusable in interactive mode (leak on Undo). With this patch the opaque tables are functional and part of the env. I.e. a constant_body can point to the proof term in 2 ways: 1) directly (before the constant is discharged) 2) indirectly, via an int, that is mapped by the opaque table to the proof term. This is now consistent in batch/interactive mode This is step 0 to make an interactive coqtop able to dump a .vo/.vi | |||
| 2014-10-13 | Coqinit: look in toploop/ even if configured with -local | Enrico Tassi | |
| 2014-10-13 | Mentioning incompatibility shown in #3718 and coming from #3050 | Hugo Herbelin | |
| (interpreting "match goal"'s hypotheses in scope %type). | |||
| 2014-10-12 | Tentative fix for a badly used Option.get in Reductionops. | Pierre-Marie Pédrot | |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau | |
| for the record binder of classes. This name is no longer generated in the kernel but part of the declaration. Also cleanup the interface to recognize primitive records based on an option type instead of a dynamic check of the length of an array. | |||
| 2014-10-10 | Do not expand primitive projections eagerly in evarconv, but only | Matthieu Sozeau | |
| in cases of unification with existentials requiring it. | |||
| 2014-10-10 | Give the same argument name for the record binder of type class | Matthieu Sozeau | |
| projections and regular records. Easily fixable backwards incompatibility. | |||
| 2014-10-10 | Add debug printers for projections, fix printing of evar constraints | Matthieu Sozeau | |
| and unsatisfiable constraints which were not done in the right environment. | |||
| 2014-10-10 | Add a "Debug Tactic Unification" option and correct the first-order | Matthieu Sozeau | |
| application case to expand primitive projections at the head of both applications. | |||
| 2014-10-10 | Make constrMatching and detyping more robust with respect to | Matthieu Sozeau | |
| expand_projection failing if an innapropriate sigma is given. | |||
| 2014-10-10 | Fix bug due to shadowing a variable name in tacred | Matthieu Sozeau | |
| 2014-10-10 | Fix segfault in native compiler on int31 division. | Maxime Dénès | |
| Thanks to Yves for reporting it! | |||
| 2014-10-09 | No need anymore for referring to xml directory in MLINCLUDES. | Hugo Herbelin | |
| 2014-10-09 | Restoring plugins/xml/README erased by mistake. | Hugo Herbelin | |
| 2014-10-09 | Propagating name of goal to main subgoal in cut and conversion tactics. | Hugo Herbelin | |
| 2014-10-09 | Added support for having one subgoal inheriting the name of its father in ↵ | Hugo Herbelin | |
| Refine. | |||
| 2014-10-09 | Removing Convert_concl and Convert_hyp from Logic. | Hugo Herbelin | |
| 2014-10-09 | A version of convert_concl and convert_hyp in new proof engine. | Hugo Herbelin | |
| Not very optimized though (if we apply convert_hyp on any hyp, a new evar will be generated for every different hyp...). | |||
| 2014-10-09 | Adding printer for named_context_val and Goal.goal in debugger. | Hugo Herbelin | |
| 2014-10-09 | Fixup leading ./ path cleaning | Pierre Boutillier | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |