| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-19 | Print [uconstr] in genargs. | Arnaud Spiwack | |
| 2014-11-19 | Print [uconstr]-s in [idtac] messages. | Arnaud Spiwack | |
| 2014-11-19 | Proper printer for [uconstr] in [Pptactic]. | Arnaud Spiwack | |
| This particular instance is probably never called though. | |||
| 2014-11-19 | Printing function for [uconstr]. | Arnaud Spiwack | |
| The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure. | |||
| 2014-11-19 | uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and ↵ | Arnaud Spiwack | |
| pattern-matching. In the syntax [let (x1,…,xn) := b in e] the name [x1…xn] were not interpreted with respect to the Ltac context. Hence typeable term would raise type-errors. The same problem also existed in pattern-matching. | |||
| 2014-11-19 | Glob-ops: a name-mapping operation for pattern-matching binders. | Arnaud Spiwack | |
| 2014-11-19 | Adding rich-printing facilities to Printmod. | Pierre-Marie Pédrot | |
| 2014-11-18 | Tentative rephrasing of error message for rewrite. | Hugo Herbelin | |
| 2014-11-18 | Hopefully the last word on having "simpl f" complying with the | Hugo Herbelin | |
| semantics described in the reference manual (i.e. if "f" is a qualid, do not add implicit arguments and, a fortiori, do not try to solve these implicit arguments - in particular, changing DbLib which expected this rule not to be followed). | |||
| 2014-11-18 | Fixing a little bug with nested but convertible occurrences in "destruct at". | Hugo Herbelin | |
| 2014-11-18 | Fixing detection of occurrences in the presence of nested subterms for | Hugo Herbelin | |
| "simpl at" and "change at". | |||
| 2014-11-18 | Clarifying the role of ListSet.v in the library, compared to other | Hugo Herbelin | |
| finite set libraries. | |||
| 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". | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |