| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-26 | Fixing Coq compilation. | Pierre-Marie Pédrot | |
| 2014-11-26 | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin | |
| in tactic unification. | |||
| 2014-11-26 | Registering strict implicit arguments systematically. | Hugo Herbelin | |
| 2014-11-25 | Bug #3804 is actually closed (thanks to Jason Gross for the notification). | Xavier Clerc | |
| 2014-11-25 | Tweak some test cases. | Xavier Clerc | |
| 2014-11-25 | Fix order of arguments in Extract Constant for Pos.compare_cont. | Maxime Dénès | |
| 2014-11-25 | Adding tag output to references in Ppconstr. | Pierre-Marie Pédrot | |
| 2014-11-25 | Used an evar name based on the local def name in "evar" tactic. | Hugo Herbelin | |
| 2014-11-25 | A bit more information in debug tactic unification. | Hugo Herbelin | |
| 2014-11-25 | Adapting to current semantics of "simpl non-evaluable-cst" | Hugo Herbelin | |
| 2014-11-25 | Experimenting using unification when matching evar/meta free subterms | Hugo Herbelin | |
| while before these were supposed to consider only syntactically. Made the experiment to unify with all delta flags unset. Keeping the same flags as for non evar/meta free subterms would lead to too much successes, as e.g. "true && b" matching "b" when the modulo_conv_on_closed_terms flag is set, which is the case for rewrite. But maybe should we instead investigate to have the same flags but with the restrict_conv_on_strict_subterms flag set. This rules out examples like "true && b" unifying with "b" and this is another option which is ok for compiling the stdlib without any changes. | |||
| 2014-11-24 | Plugging console highlighting in for toplevel and compilation error messages. | Pierre-Marie Pédrot | |
| 2014-11-24 | Adding test for bug #3248. | Pierre-Marie Pédrot | |
| 2014-11-24 | Fixing bug #3817. | Pierre-Marie Pédrot | |
| Coqtop was wrongly assuming that receiving a SIGINT when reading on a channel meant that the channel was closed, resulting in a crash when interrupting an idle coqtop from CoqIDE. To prevent this, we block SIGINTs when reading in ide_slave. | |||
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau | |
| inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821). | |||
| 2014-11-23 | One more word about "simpl f": avoid "simpl f" to be printed "simpl f", | Hugo Herbelin | |
| at least when f is an evaluable reference. | |||
| 2014-11-23 | Add printer for transparent state for ocamldebug. | Hugo Herbelin | |
| 2014-11-23 | Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc about | Hugo Herbelin | |
| when the arguments of a constructor can be moved at the place of the variable on which destruct or induction applies. | |||
| 2014-11-23 | Fix #3824. de Bruijn error in normalization of fixpoints. | Maxime Dénès | |
| This bug was affecting the VM and the native compiler, but only in the pretyper (not the kernel). Types of arguments of fixpoints were incorrectly normalized due to a missing lift. | |||
| 2014-11-22 | Specific printer of Evar.Set.t for ocamldebug + more information in | Hugo Herbelin | |
| a UserError to ease debugging. | |||
| 2014-11-22 | Attempt to organize and document unification flags of setoid rewrite. | Hugo Herbelin | |
| 2014-11-22 | Removing superfluous newlines in setoid_rewrite error message. | Hugo Herbelin | |
| 2014-11-22 | In setoid_rewrite error messages: | Hugo Herbelin | |
| - removed the encapsulation in a Tactic Failure (I don't see why setoid_rewrite should specifically raise a Fail - do I miss something?) - avoid having twice a "Unable to satisfy ... constraints" message. | |||
| 2014-11-22 | Test for closed #2713 and #2876. | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |