aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Removing dead unsafe debugging code in Constrintern.Gravatar Pierre-Marie Pédrot2016-08-16
|
* Merge PR #250 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
* \ Merge PR #237 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\ \
* \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\ \ \
* \ \ \ Efficiently generate the pretyping contexts.Gravatar Pierre-Marie Pédrot2016-08-16
|\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We used to recompute all fresh named contexts for evars before this patch in the push_rel_context_to_named_context function. This was incurring a linear penalty and a memory explosion due to the reallocation of many arrays. Now, we rather remember the context between evar creations by sharing it in the pretyping environment. This can be considered as a fix for bug #4964 even though we might do better.
| | * \ \ Merge branch 'pr255' into v8.5 (bug #5015)Gravatar Guillaume Melquiond2016-08-16
| | |\ \ \
| | | * | | Fix regression in Coqide's "forward one command" commandGravatar Xavier Leroy2016-08-14
| | |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".". In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed. I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
| | * | | Do not assume the "TERM" environment variable is always set (bug #5007).Gravatar Guillaume Melquiond2016-08-11
| | | | |
| | * | | Use the "md5" command on OpenBSD (bug #5008).Gravatar Guillaume Melquiond2016-08-11
| | | | |
* | | | | Make code a bit clearer by removing optional argument.Gravatar Guillaume Melquiond2016-08-10
| | | | |
* | | | | Remove unused optional "predicative" argument.Gravatar Guillaume Melquiond2016-08-10
| | | | |
* | | | | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
| | | | |
* | | | | Reduce warning noise when compiling the standard library.Gravatar Guillaume Melquiond2016-08-09
| | | | |
* | | | | Make List.map_filter(_i) tail-recursive.Gravatar Guillaume Melquiond2016-08-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | While the performance gain should go unnoticed in most cases, in some degenerate situations, e.g. the evar-stressing test-case of bug #4964, this commit speeds up coq by 10% since most of the time is spent scanning long lists with most of the elements filtered out. Note that this commit also changes the scanning order to front-to-back, which is a bit less surprising (though no code should ever depend on the scanning order).
| | * | | Fix #5000: Document the native compiler soundness bug due to Unicode mangling.Gravatar Pierre-Marie Pédrot2016-08-07
| | | | |
| * | | | Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
| | | | | | | | | | | | | | | | | | | | This saves a quadratic allocation by replacing arrays with maps.
| * | | | Using the extended contexts in pretyping.Gravatar Pierre-Marie Pédrot2016-08-05
| | | | | | | | | | | | | | | | | | | | | | | | | In addition to sharing, we also delay the computation of the environment in a by-need fashion.
| * | | | Use sets instead of lists for names to avoid in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
| | | | |
| * | | | Simplifying code in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences.
| * | | | Exporting the renaming API for evar declaration.Gravatar Pierre-Marie Pédrot2016-08-04
| | | | |
| * | | | Embedding the pretyping environment in a dummy record.Gravatar Pierre-Marie Pédrot2016-08-04
|/ / / /
| * | | Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
| | | |
| * | | Fix bug #4673: regression in setoid_rewrite.Gravatar Matthieu Sozeau2016-07-29
| | | | | | | | | | | | | | | | Modulo delta for types should be fully transparent.
* | | | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\| | |
| * | | Update CHANGES about #3886 bugfixGravatar Matthieu Sozeau2016-07-29
| | | |
| * | | Fix bug #3886, generation of obligations of fixesGravatar Matthieu Sozeau2016-07-29
| | | | | | | | | | | | | | | | This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
| * | | Fix #4769, univ poly and elim schemes in sectionsGravatar Matthieu Sozeau2016-07-29
| | | |
* | | | COMMENT: moving misplaced comment where it belongsGravatar Matej Kosik2016-07-29
| | | |
* | | | Adding a flag in CoqIDE to configure UNIX/Windows line ending.Gravatar Pierre-Marie Pédrot2016-07-26
| | | | | | | | | | | | | | | | Fixes both bugs #4924 and #4437.
* | | | restore compatibility with gallium's camlp4 (broken by commit 8e07227c)Gravatar Pierre Letouzey2016-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Apparently, in camlp4 (unlike camlp5) : - Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]" produces a kwd of type token instead of string (which sounds reasonable ?). For now, I've replaced kwd by the explicit strings. Not so nice, but works with both camlp4 and camlp5 - A quotation of the form "let obj = ... in bar; baz" is not interpreted in the usual OCaml way, but rather as "(let obj = ... in bar); baz". Let's use instead "let obj = ... in let () = bar in baz", which works fine.
| * | | Update CHANGES about critical bugfix and othersGravatar Matthieu Sozeau2016-07-26
| | | |
| * | | Merge branch 'bug4754' into v8.5Gravatar Matthieu Sozeau2016-07-26
| |\ \ \
| | * | | Fix bug #4754, allow conversion problems to remainGravatar Matthieu Sozeau2016-07-26
| |/ / / | | | | | | | | | | | | | | | | when checking that the rewrite relation is homogeneous in setoid_rewrite.
* | | | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\| | |
| * | | Merge branch 'bug4876' into v8.5Gravatar Matthieu Sozeau2016-07-26
| |\ \ \
* | \ \ \ Merge remote-tracking branch 'github/bug4679' into v8.6Gravatar Matthieu Sozeau2016-07-25
|\ \ \ \ \
| | | * | | Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
| | |/ / /
| * | | | Fix bug #4679, weakened setoid_rewrite unificationGravatar Matthieu Sozeau2016-07-21
| | | | | | | | | | | | | | | | | | | | | | | | | It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4.
* | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-20
|\ \ \ \ \ | |/ / / / |/| / / / | |/ / /
| * | | Update CHANGESGravatar Matthieu Sozeau2016-07-20
| | | |
| * | | Fix bug #4780: universe leak in letin_tacGravatar Matthieu Sozeau2016-07-20
| | | |
* | | | Update CHANGESGravatar Matthieu Sozeau2016-07-20
| | | |
* | | | Fix bug #4780: universe leak in letin_tacGravatar Matthieu Sozeau2016-07-20
| | | |
| | | * Allow `STDTIME=foo make`Gravatar Jason Gross2016-07-19
| |_|/ |/| | | | | This gives better behavior both when including the `coq_makefile` `Makefile` into other `Makefile`s and when setting `STDTIME` through an environment variable.
| * | Fix Errors.out missing a dot...Gravatar Matthieu Sozeau2016-07-19
| | |
* | | Complementing previous commit on fixes for printing binding patterns.Gravatar Hugo Herbelin2016-07-19
| | |
* | | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
* | | Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | | | | Supporting accordingly printing of sequences of binders including binding patterns.
* | | Notations with multiple recursive binders: fixing use of alpha-conversion.Gravatar Hugo Herbelin2016-07-19
| | |
* | | Fixing missing parentheses in printing of patterns in binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | (In agreement with Daniel.)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 02:59:51 +0000