| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-07-25 | Add a tactic [swap i j] to swap the position of goals [i] and [j]. | Arnaud Spiwack | |
| If [i] or [j] is negative goals are counted from the end. | |||
| 2014-07-25 | Adds a cycle tactic to reorder goals in a loop. | Arnaud Spiwack | |
| [cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1]. | |||
| 2014-07-25 | A slightly more fine grained way to check whether a TACTIC EXTEND is global ↵ | Arnaud Spiwack | |
| or local to goals. Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global. | |||
| 2014-07-25 | CHANGES: yellow in Coqide. | Arnaud Spiwack | |
| 2014-07-25 | CHANGE: add Derive. | Arnaud Spiwack | |
| 2014-07-25 | CHANGE: document the features of the new tactic engine. | Arnaud Spiwack | |
| 2014-07-25 | Update the documentation of Ltac's ";" and ";[…]" to reflect the new ↵ | Arnaud Spiwack | |
| multi-goal semantics of tactics. | |||
| 2014-07-25 | Warns about inconsistency of generated name in evars and goals. | Arnaud Spiwack | |
| See bug #1041 | |||
| 2014-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau | |
| - Distinguish between primitive and non-primitive records in the kernel declaration, so as to try eta-conversion on primitive records only. | |||
| 2014-07-25 | More documentation of universes. | Matthieu Sozeau | |
| 2014-07-25 | Add emacs auto-save and crash-save files to the .gitignore. | Arnaud Spiwack | |
| 2014-07-25 | Add *.crashcoqide files to the .gitignore. | Arnaud Spiwack | |
| They occasionally show up while testing. I think it cleaner to ignore them. | |||
| 2014-07-25 | Add lia.cache to the .gitignore | Arnaud Spiwack | |
| 2014-07-25 | Small reorganisation in proof.ml. | Arnaud Spiwack | |
| 2014-07-25 | Fail gracefully when focusing on non-existing goals with user commands. | Arnaud Spiwack | |
| Fixes bug #3457 | |||
| 2014-07-25 | Fix handling of universes at the end of proofs, esp. for async proof processing. | Matthieu Sozeau | |
| Thanks to E. Tassi for the initial patch. | |||
| 2014-07-24 | Forgot to add a Universes.v.tex as a target. | Matthieu Sozeau | |
| 2014-07-24 | Start documenting universe polymorphism. | Matthieu Sozeau | |
| 2014-07-24 | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack | |
| 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. | |||
| 2014-07-24 | A handful of useful primitives in Proofview.Refine. | Arnaud Spiwack | |
| 2014-07-24 | Fix misleading pretty-printing of information for non-universe-polymorphic | Matthieu Sozeau | |
| definitions. | |||
| 2014-07-24 | Adding a tail-rec tclONCE. | Pierre-Marie Pédrot | |
| 2014-07-24 | New implementation of the tactic monad. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-07-24 | Revert "Adding a "is_val" primitive to IStream." | Pierre-Marie Pédrot | |
| This reverts commit 062d07eb5446c1032fda232b9a09e20e5410dd92. | |||
| 2014-07-24 | fixup fakeide test-suite | Pierre Boutillier | |
| 2014-07-24 | Make MacStore like coqide more | Pierre Boutillier | |
| including bigger icons | |||
| 2014-07-23 | Derive plugin: document new syntax. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: add some comments. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: code reorganisation for clarity. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: small refactoring. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: a more general interface. | Arnaud Spiwack | |
| Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def. | |||
| 2014-07-23 | When closing a proof, make sure that the types have their evar substituted. | Arnaud Spiwack | |
| 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. | |||
| 2014-07-23 | Proof_global: an unused variable replaced by a wildcard. | Arnaud Spiwack | |
| 2014-07-23 | Proof_global.start_dependent_proof: properly threads the sigma through the ↵ | Arnaud Spiwack | |
| telescope. Allows for a more refined notion of dependently generated initial goals. | |||
| 2014-07-23 | Change the interface of proof_global to take an evar_map instead of a ↵ | Arnaud Spiwack | |
| 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. | |||
| 2014-07-22 | Porting guard fix to checker. | Maxime Dénès | |
| 2014-07-22 | Minor cleaning. | Maxime Dénès | |
| 2014-07-22 | Revert "Extend subterm relation to pattern matching in return predicates." | Maxime Dénès | |
| This reverts commit ec1bb8a981fef14b58ab65483244fc42b05aef13. | |||
| 2014-07-22 | Revert "Propagate size info through pattern matching in predicates, for the" | Maxime Dénès | |
| This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea. Apply again if this kind of dependently typed programming idioms are needed. | |||
| 2014-07-22 | Propagate size info through pattern matching in predicates, for the | Maxime Dénès | |
| commutative cut rule. The error messages of the guard checker are now sometimes not informative enough. | |||
| 2014-07-22 | Extend subterm relation to pattern matching in return predicates. | Maxime Dénès | |
| 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. | |||
| 2014-07-22 | Fix check_inductive_codomain. | Maxime Dénès | |
| 2014-07-22 | Refine check_is_subterm. | Maxime Dénès | |
| 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. | |||
| 2014-07-22 | Refined guard condition of cofixpoints, to anticipate potential futur | Maxime Dénès | |
| extensions. | |||
| 2014-07-22 | First attempt at a fix for guard condition on cofixpoints. | Maxime Dénès | |
| 2014-07-22 | Add test-suite file for guard condition on cofixpoints. | Maxime Dénès | |
| 2014-07-22 | Typo in comment. | Maxime Dénès | |
| 2014-07-22 | Simplified rect2, it turns out Arthur's trick was not required. | Maxime Dénès | |
| Standard library now compiles fully. | |||
| 2014-07-22 | A version of Fin.rect2 that is compatible with the fix of the guard condition. | Maxime Dénès | |
| Thanks to Arthur Azevedo de Amorim! | |||
| 2014-07-22 | Fixed proof of irrelevance of le on nat, inspired by the | Maxime Dénès | |
| corresponding proof in ssreflect. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |