| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-10-09 | Coq_makefile: Allow empty logical names | Pierre Boutillier | |
| I'm not sure that coqdep and coqtop understand them correctly anyway ... | |||
| 2014-10-08 | fix make mlidoc | Pierre Boutillier | |
| 2014-10-08 | Fixing the anomaly in bug #3045 (a filter was not type-safe in | Hugo Herbelin | |
| 2nd-order matching). We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is well-typed when taking the filtered context Gamma) in 2nd order matching. Maybe this weakens the power of the 2nd order matching algorithm, so it is not clear that it is the good fix. Another fix could have been to ensure that taking the closure of filter does not extend it beyond the original filter (hence keeping the filter untyped if it was already untyped). As for the bug #3045, it also revealed that some "destruct c as [[]]" could be made stronger as decomposing the destruct in two parts "destruct c as [x]; destruct x" workis while it currently fails if in one part. | |||
| 2014-10-08 | Applying Virgile Prevosto's patch for better error report in coqdep (#3029). | Hugo Herbelin | |
| 2014-10-08 | Forgotten hints.ml{,i} files in 38b34dfffcc. | Hugo Herbelin | |
| 2014-10-07 | Adding a printer for hints. | Hugo Herbelin | |
| 2014-10-07 | Splitting out of auto.ml a file hints.ml dedicated to hints so as to | Hugo Herbelin | |
| being able to export hints without tactics, vm, etc. to come with. Some functions moved to the new proof engine. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |