| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-17 | Adding notation terminals to coqtop highlight. | Pierre-Marie Pédrot | |
| 2014-11-17 | Fixing semantics of Ppconstr.print_hunks. | Pierre-Marie Pédrot | |
| 2014-11-17 | Missing keywords in Ppconstr. | Pierre-Marie Pédrot | |
| 2014-11-17 | Setting printing tags for Ltac. | Pierre-Marie Pédrot | |
| 2014-11-17 | Moving printing code for red_expr and may_eval to Pptactic. | Pierre-Marie Pédrot | |
| 2014-11-17 | Documenting the -color option. | Pierre-Marie Pédrot | |
| 2014-11-17 | Documenting use of colors in Coq. | Pierre-Marie Pédrot | |
| 2014-11-17 | Default styles for printing tags. | Pierre-Marie Pédrot | |
| They should be rather sensible, but de gustibus & coloribus... | |||
| 2014-11-17 | Setting error tag on generic errors returned by Coqtop. | Pierre-Marie Pédrot | |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin | |
| reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n"). | |||
| 2014-11-16 | Fixing side bug in db37c9f3f32ae7 delaying interpretation of the | Hugo Herbelin | |
| right-hand side of a "change with": the rhs lives in the toplevel environment. | |||
| 2014-11-16 | For consistency with other coqtop flags, use -help rather than --help in usage. | Hugo Herbelin | |
| 2014-11-15 | Adding tags to messages. | Pierre-Marie Pédrot | |
| 2014-11-15 | Removing a pperrnl. | Pierre-Marie Pédrot | |
| 2014-11-15 | Adding a command line option to print out accepted color tags. | Pierre-Marie Pédrot | |
| 2014-11-15 | Additional style tags for constrs. | Pierre-Marie Pédrot | |
| 2014-11-15 | Reworking the -color flag of coqtop. | Pierre-Marie Pédrot | |
| 2014-11-15 | Removing deprecated code handling color in Pp. | Pierre-Marie Pédrot | |
| 2014-11-15 | Setting a keyword tag in Ppconstr. | Pierre-Marie Pédrot | |
| 2014-11-15 | Plugging the color initialization in the Coqtop loop. | Pierre-Marie Pédrot | |
| 2014-11-15 | Adding a pretty-printing style library. | Pierre-Marie Pédrot | |
| 2014-11-15 | Adding a terminal library. | Pierre-Marie Pédrot | |
| 2014-11-14 | Use return code to classify anomalies as active open bugs. | Xavier Clerc | |
| 2014-11-14 | Exit with code 129 when an anomaly occurs. | Xavier Clerc | |
| 2014-11-14 | Get rif of exit codes 120, 121, 123, and 124. | Xavier Clerc | |
| 2014-11-14 | Add missing "Fail" to test case for bug #2814. | Xavier Clerc | |
| 2014-11-14 | Reproduction cases for the test suite. | Xavier Clerc | |
| 2014-11-14 | Preserving the good effect of 014e5ac92a on not leaving dangling local | Hugo Herbelin | |
| definitions while keeping some compatibility on when to generalize when an index also occur in a parameter (effect on PersistentUnionFind for instance). | |||
| 2014-11-13 | Fixing Scheme Equality, after bug introduced in bf018569405c. | Hugo Herbelin | |
| 2014-11-13 | Move conjugate_verb_to_be next to cString.plural. | Hugo Herbelin | |
| 2014-11-13 | Removing yet another source of remaining local definitions. | Hugo Herbelin | |
| 2014-11-12 | Document (some) Proof using syntax + the new Optimize commands | Enrico Tassi | |
| 2014-11-12 | Cleaner interfaces for linking locations of native compiler. | Maxime Dénès | |
| Stop sharing those references across constants of the same module, which was triggering some bugs when using native_compute in interactive mode in a functor declaration. | |||
| 2014-11-11 | Accepting conversion on inner closed subterms while looking for | Hugo Herbelin | |
| matching subterm destruct/induction on a partially applied pattern. AFAICS, there is only such instance of destruct that needs this in the contrins (in EuclideanGeometry/G3_ParticularAngle.v), but while a more global decision is taken, I prefer at the current time to adopt this approximation of 8.4 semantics, even if the flags are not the same when the pattern is fully applied or not. Only so little cases are concerned because in most cases, destruct/induction on a partially applied pattern is of the form "destruct cst" (e.g. "destruct eq_dec") and no conversion is needed anyway. Not being uniform whether the pattern is fully applied or not is a bit unsatisfactory, but hopefully, this is temporary. | |||
| 2014-11-11 | Adapting output tests to current naming of evars, even if unclear | Hugo Herbelin | |
| where it will eventually stabilize. | |||
| 2014-11-11 | Updating CHANGES (evars as ident). | Hugo Herbelin | |
| 2014-11-11 | American spelling + layout in CHANGES. | Hugo Herbelin | |
| 2014-11-11 | Renouncing to check only at the end of the call to "apply in" the | Hugo Herbelin | |
| absence of remaining dependent evars when several arguments are given. For simplicity of implementation, checking instead for every step of the n-ary "apply in". | |||
| 2014-11-10 | Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly. | Pierre-Marie Pédrot | |
| This is a continuation of the previous patch. | |||
| 2014-11-10 | Evar normalization is now done eagerly. | Pierre-Marie Pédrot | |
| As witnessed in the ProjectiveGeometry contrib, some evar normalization were taking ages because of an exponential behaviour due to a call-by-name substitution: when normalizing an evar, its arguments were substituted right away and the resulting term was then normalized, leading to a potential duplication of normalizations. Now we normalize evar arguments before substituting them, in a call-by-value fashion. It makes examples from ProjectiveGeometry compile instanteanously when they were killing the machine due to excessive memory allocation before the patch. Note that there is a tension here: we may be normalizing evar arguments too eagerly, and try a call-by-need approach instead. To choose which particular strategy we use, we should do some benchmarks... On stdlib, call-by-value and call-by-need seem indistinguishable. To be continued? | |||
| 2014-11-10 | Fix #3282: VM confused by let bindings in fixpoints. | Maxime Dénès | |
| I'm afraid this fix is a bit heuristic, but it seems to generate correct code in all cases. | |||
| 2014-11-10 | Better printing of dynlink errors in native compiler. | Maxime Dénès | |
| 2014-11-10 | Plug the dynamic tags in the Richpp mechanism. | Pierre-Marie Pédrot | |
| 2014-11-10 | Adding a dynamic tag type in Pp. | Pierre-Marie Pédrot | |
| 2014-11-10 | Replugging hints in rewriting strategies. | Pierre-Marie Pédrot | |
| 2014-11-10 | Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3). | Pierre-Marie Pédrot | |
| 2014-11-09 | Fixing bug #3803. | Pierre-Marie Pédrot | |
| The Info layer was setting the required evarmap too eagerly, making the tclWITHHOLE tactical accept terms with holes. The logging facility is now inside the tclWITHHOLES. | |||
| 2014-11-09 | Removing the unused boolean flag from the move tactic implementation. | Pierre-Marie Pédrot | |
| 2014-11-09 | Removing a unused boolean in the TacMove node of tacexpr AST. | Pierre-Marie Pédrot | |
| 2014-11-09 | Adding test for bug 3792. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |