| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-20 | Moving mutual inductive printing from Printer to Printmod. | Pierre-Marie Pédrot | |
| 2014-11-19 | Making map_union a standard function of the ML library. | Hugo Herbelin | |
| 2014-11-19 | Slightly improving error messages when mismatch with Proof using at Qed time. | Hugo Herbelin | |
| 2014-11-19 | Option -type-in-type continued (deactivate test for inferred sort of | Hugo Herbelin | |
| inductive types + deactivate test for equality of sort + deactivate the check that the constraints Prop/Set <= Type are declared). | |||
| 2014-11-19 | Continuing fixing nested but convertible occurrences in find_subterm | Hugo Herbelin | |
| (see 2e3ae20fe1e): test was only relevant in the case of explicitly given occurrence numbers. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |