aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Update the documentation of Ltac's ";" and ";[…]" to reflect the new ↵Gravatar Arnaud Spiwack2014-07-25
| | | | multi-goal semantics of tactics.
* Warns about inconsistency of generated name in evars and goals.Gravatar Arnaud Spiwack2014-07-25
| | | | See bug #1041
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
| | | | | - Distinguish between primitive and non-primitive records in the kernel declaration, so as to try eta-conversion on primitive records only.
* More documentation of universes.Gravatar Matthieu Sozeau2014-07-25
|
* Add emacs auto-save and crash-save files to the .gitignore.Gravatar Arnaud Spiwack2014-07-25
|
* Add *.crashcoqide files to the .gitignore.Gravatar Arnaud Spiwack2014-07-25
| | | They occasionally show up while testing. I think it cleaner to ignore them.
* Add lia.cache to the .gitignoreGravatar Arnaud Spiwack2014-07-25
|
* Small reorganisation in proof.ml.Gravatar Arnaud Spiwack2014-07-25
|
* Fail gracefully when focusing on non-existing goals with user commands.Gravatar Arnaud Spiwack2014-07-25
| | | Fixes bug #3457
* Fix handling of universes at the end of proofs, esp. for async proof processing.Gravatar Matthieu Sozeau2014-07-25
| | | | Thanks to E. Tassi for the initial patch.
* Forgot to add a Universes.v.tex as a target.Gravatar Matthieu Sozeau2014-07-24
|
* Start documenting universe polymorphism.Gravatar Matthieu Sozeau2014-07-24
|
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
| | | They used to be the same (and had a single entry in the AST). But now that t2 can be a multi-goal tactic, t1;[t2..] has the semantics of executing t2 in each goal independently.
* A handful of useful primitives in Proofview.Refine.Gravatar Arnaud Spiwack2014-07-24
|
* Fix misleading pretty-printing of information for non-universe-polymorphicGravatar Matthieu Sozeau2014-07-24
| | | | definitions.
* Adding a tail-rec tclONCE.Gravatar Pierre-Marie Pédrot2014-07-24
|
* New implementation of the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-24
| | | | | | | | | The new implementation is made of two layers: a iolist, which is essentially a stream without memoization, and above this a state monad. The previous design of the extracted monad kept three distinct but similar monad transformers: a stateT, a writerT and a readerT. We take advantage of this similarity to pack those three transformers into only one state monad. This makes the code cleaner and hopefully more efficient.
* Revert "Adding a "is_val" primitive to IStream."Gravatar Pierre-Marie Pédrot2014-07-24
| | | | This reverts commit 062d07eb5446c1032fda232b9a09e20e5410dd92.
* fixup fakeide test-suiteGravatar Pierre Boutillier2014-07-24
|
* Make MacStore like coqide moreGravatar Pierre Boutillier2014-07-24
| | | | including bigger icons
* Derive plugin: document new syntax.Gravatar Arnaud Spiwack2014-07-23
|
* Derive plugin: add some comments.Gravatar Arnaud Spiwack2014-07-23
|
* Derive plugin: code reorganisation for clarity.Gravatar Arnaud Spiwack2014-07-23
|
* Derive plugin: small refactoring.Gravatar Arnaud Spiwack2014-07-23
|
* Derive plugin: a more general interface.Gravatar Arnaud Spiwack2014-07-23
| | | | Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.
* When closing a proof, make sure that the types have their evar substituted.Gravatar Arnaud Spiwack2014-07-23
| | | | When starting proofs with [start_dependent_proof], we may have initial goals with existential variables in their conclusion. They will be solved by the proof, but this information was not propagated in close proof, and the kernel failed on uninstanciated evars.
* Proof_global: an unused variable replaced by a wildcard.Gravatar Arnaud Spiwack2014-07-23
|
* Proof_global.start_dependent_proof: properly threads the sigma through the ↵Gravatar Arnaud Spiwack2014-07-23
| | | | | telescope. Allows for a more refined notion of dependently generated initial goals.
* Change the interface of proof_global to take an evar_map instead of a ↵Gravatar Arnaud Spiwack2014-07-23
| | | | | universe context to start proofs. It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.
* Porting guard fix to checker.Gravatar Maxime Dénès2014-07-22
|
* Minor cleaning.Gravatar Maxime Dénès2014-07-22
|
* Revert "Extend subterm relation to pattern matching in return predicates."Gravatar Maxime Dénès2014-07-22
| | | | This reverts commit ec1bb8a981fef14b58ab65483244fc42b05aef13.
* Revert "Propagate size info through pattern matching in predicates, for the"Gravatar Maxime Dénès2014-07-22
| | | | | | This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea. Apply again if this kind of dependently typed programming idioms are needed.
* Propagate size info through pattern matching in predicates, for theGravatar Maxime Dénès2014-07-22
| | | | | | | commutative cut rule. The error messages of the guard checker are now sometimes not informative enough.
* Extend subterm relation to pattern matching in return predicates.Gravatar Maxime Dénès2014-07-22
| | | | | | | | | | A pattern matching is can now be a subterm if: - Every branch is a subterm - The return predicate is a pattern matching whose return predicate is an arity. - That pattern matching (in the return predicate) returns the same inductive family in the conclusion of each branch. The commutative cut rule hasn't been updated accordingly yet.
* Fix check_inductive_codomain.Gravatar Maxime Dénès2014-07-22
|
* Refine check_is_subterm.Gravatar Maxime Dénès2014-07-22
| | | | | | | Following Bruno's suggestion, we check if the tree expected for the recursive argument is included in the one which is inferred. This check is probably not necessary in the current state of affairs, but might become so after further extensions of the guard condition.
* Refined guard condition of cofixpoints, to anticipate potential futurGravatar Maxime Dénès2014-07-22
| | | | extensions.
* First attempt at a fix for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
|
* Add test-suite file for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
|
* Typo in comment.Gravatar Maxime Dénès2014-07-22
|
* Simplified rect2, it turns out Arthur's trick was not required.Gravatar Maxime Dénès2014-07-22
| | | | Standard library now compiles fully.
* A version of Fin.rect2 that is compatible with the fix of the guard condition.Gravatar Maxime Dénès2014-07-22
| | | | Thanks to Arthur Azevedo de Amorim!
* Fixed proof of irrelevance of le on nat, inspired by theGravatar Maxime Dénès2014-07-22
| | | | corresponding proof in ssreflect.
* Made intersection on regular trees less intensional.Gravatar Maxime Dénès2014-07-22
|
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
| | | | | | instantiated in the return predicate are now taken into account. The resulting recargs tree is the intersection between the one of the branches and the appearing in the return predicate. Both the domain and co-domain are filtered.
* Tentative fix for the commutative cut subterm rule.Gravatar Maxime Dénès2014-07-22
| | | | | Some fixpoints are now rejected in the standard library, but that's probably because we compare trees for equality instead of intersecting them.
* Tentative patch for incompatibility between subterm relation and dependentGravatar Maxime Dénès2014-07-22
| | | | | | | | | | | | pattern matching. This patch should be improved in two ways: (1) Implement the same checks for the commutative cut subterm rule. (2) When checking safe recursive subterms for each of the branches in a match, instanciated parameters in the return predicate should be taken into account. Step (1) should be enough to restore a correct guard condition, but (2) will be required if we don't want to rule out some legitimate and practical examples.
* Ide: Drop argument added by MacOS during .app launchGravatar Pierre Boutillier2014-07-22
|
* the art of forgetting new files during rebase -iGravatar Pierre Boutillier2014-07-22
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 09:27:20 +0000