| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-22 | Removing useless flag of the historical move tactic. | Pierre-Marie Pédrot | |
| 2014-11-22 | Exporting a primitive allowing to run completely the tactic monad. | Pierre-Marie Pédrot | |
| 2014-11-21 | Adding test for bug #3326. | Pierre-Marie Pédrot | |
| 2014-11-21 | Adding test for bug #3424. | Pierre-Marie Pédrot | |
| 2014-11-21 | Cleaning up closed bugs in test-suite. | Pierre-Marie Pédrot | |
| 2014-11-21 | Writing Tactics.keep in the new monad. | Pierre-Marie Pédrot | |
| 2014-11-21 | Test for bug #3788. | Pierre-Marie Pédrot | |
| 2014-11-21 | Add test-suite file for bug #3804. | Matthieu Sozeau | |
| 2014-11-21 | Fix bug #3804. | Matthieu Sozeau | |
| 2014-11-21 | Avoid compilation warning. | Matthieu Sozeau | |
| 2014-11-20 | Adding test for bug #3684. | Pierre-Marie Pédrot | |
| 2014-11-20 | Fixing the previous commit. We had to normalize evars first. | Pierre-Marie Pédrot | |
| 2014-11-20 | Somehow fixing a side-effect bug in tactics-in-terms. | Pierre-Marie Pédrot | |
| Before this patch, when tactics-in-terms were relying on the ugly environment- modifying primitives such as tclABSTRACT, the returned term was ill-typed because the resulting effects were just dropped. Now we modify the returned term on the fly, effectively getting rid of the effects it may depend on. Yet, this is not completely satisfactory, because the tactic may solve some goals at distance (I would have said by side-effect, but this is ambiguous here). If ever the resulting terms are depending on the side-effects of the tactic, then we are still unsound. This patch should handle most of the use-cases gracefully. To really solve this issue, we should rewrite the pretyper in the new monad, which is easier said than done. | |||
| 2014-11-20 | Probably useless use of a global-environment reading function in Indrec. | Pierre-Marie Pédrot | |
| 2014-11-20 | Exporting the function handling side-effects only applied to terms. | Pierre-Marie Pédrot | |
| 2014-11-20 | Re-removing the Hiddentac module. For some reason it had been reintroduced | Pierre-Marie Pédrot | |
| by commit bf0185694. | |||
| 2014-11-20 | Global.env chasing in Inv. | Pierre-Marie Pédrot | |
| 2014-11-20 | Adding locations to tclZEROMSG. | Pierre-Marie Pédrot | |
| 2014-11-20 | Setting printing flags on the printing of mutual inductives. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |