| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-22 | Further simplifying functional induction. | Hugo Herbelin | |
| 2014-11-22 | Simplifying code of functional induction. | Hugo Herbelin | |
| 2014-11-22 | Not using an (arbitrary) pivot anymore for re-introduction of | Hugo Herbelin | |
| quantified hypothesis in functional induction. This has apparently no visible effect, probably because functional schemes do not have non-dependent hypothesis in their branches besides induction hypotheses which are anyway introduced at the top of the context. | |||
| 2014-11-22 | New simplification of code for generalizing hypotheses in destruct. | Hugo Herbelin | |
| 2014-11-22 | Removing a hack which, according to the comment, should not be necessary | Hugo Herbelin | |
| anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)". | |||
| 2014-11-22 | Add test-suite file for dependent rewriting example by Vadim Zaliva and | Matthieu Sozeau | |
| Daniel Schepler. | |||
| 2014-11-22 | Fix resolve_morphism to build well-scoped terms in case some arguments | Matthieu Sozeau | |
| of the function are dependent. | |||
| 2014-11-22 | Enforcing the non-normalization of evars in Tactics.get_next_hyp_position. | Pierre-Marie Pédrot | |
| 2014-11-22 | Writing intro_replacing in the new monad. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |