aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-07-29Add test-suite file for bug #3453Matthieu Sozeau
2014-07-29Fix bug #3453, not recognizing primitive projections in Coercion declarations.Matthieu Sozeau
2014-07-29Fix treatment of notations containing applications of projections (fixes bug ...Matthieu Sozeau
2014-07-29STM: print goals with no duplicatesEnrico Tassi
2014-07-29Pp: only one default feedback idEnrico Tassi
2014-07-29Pp compiles after feedbackEnrico Tassi
2014-07-28CPS-style tactic matching. We use the tactic monad as the target of the CPS.Pierre-Marie Pédrot
2014-07-28Adding a tclBREAK primitive to the tactic monad.Pierre-Marie Pédrot
2014-07-27Code cleaning in Tacenv.Pierre-Marie Pédrot
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-07-25Removing dead code relative to or_metaid.Pierre-Marie Pédrot
2014-07-25CHANGES: cycle and swap.Arnaud Spiwack
2014-07-25Document swap tactic.Arnaud Spiwack
2014-07-25Document cycle tactic.Arnaud Spiwack
2014-07-25Add a tactic [swap i j] to swap the position of goals [i] and [j].Arnaud Spiwack
2014-07-25Adds a cycle tactic to reorder goals in a loop.Arnaud Spiwack
2014-07-25A slightly more fine grained way to check whether a TACTIC EXTEND is global o...Arnaud Spiwack
2014-07-25CHANGES: yellow in Coqide.Arnaud Spiwack
2014-07-25CHANGE: add Derive.Arnaud Spiwack
2014-07-25CHANGE: document the features of the new tactic engine.Arnaud Spiwack
2014-07-25Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...Arnaud Spiwack
2014-07-25Warns about inconsistency of generated name in evars and goals.Arnaud Spiwack
2014-07-25- Do module substitution inside mind_record.Matthieu Sozeau
2014-07-25More documentation of universes.Matthieu Sozeau
2014-07-25Add emacs auto-save and crash-save files to the .gitignore.Arnaud Spiwack
2014-07-25Add *.crashcoqide files to the .gitignore.Arnaud Spiwack
2014-07-25Add lia.cache to the .gitignoreArnaud Spiwack
2014-07-25Small reorganisation in proof.ml.Arnaud Spiwack
2014-07-25Fail gracefully when focusing on non-existing goals with user commands.Arnaud Spiwack
2014-07-25Fix handling of universes at the end of proofs, esp. for async proof processing.Matthieu Sozeau
2014-07-24Forgot to add a Universes.v.tex as a target.Matthieu Sozeau
2014-07-24Start documenting universe polymorphism.Matthieu Sozeau
2014-07-24Distinguish tactics t1;t2 and t1;[t2..].Arnaud Spiwack
2014-07-24A handful of useful primitives in Proofview.Refine.Arnaud Spiwack
2014-07-24Fix misleading pretty-printing of information for non-universe-polymorphicMatthieu Sozeau
2014-07-24Adding a tail-rec tclONCE.Pierre-Marie Pédrot
2014-07-24New implementation of the tactic monad.Pierre-Marie Pédrot
2014-07-24Revert "Adding a "is_val" primitive to IStream."Pierre-Marie Pédrot
2014-07-24fixup fakeide test-suitePierre Boutillier
2014-07-24Make MacStore like coqide morePierre Boutillier
2014-07-23Derive plugin: document new syntax.Arnaud Spiwack
2014-07-23Derive plugin: add some comments.Arnaud Spiwack
2014-07-23Derive plugin: code reorganisation for clarity.Arnaud Spiwack
2014-07-23Derive plugin: small refactoring.Arnaud Spiwack
2014-07-23Derive plugin: a more general interface.Arnaud Spiwack
2014-07-23When closing a proof, make sure that the types have their evar substituted.Arnaud Spiwack
2014-07-23Proof_global: an unused variable replaced by a wildcard.Arnaud Spiwack
2014-07-23Proof_global.start_dependent_proof: properly threads the sigma through the te...Arnaud Spiwack
2014-07-23Change the interface of proof_global to take an evar_map instead of a univers...Arnaud Spiwack
2014-07-22Porting guard fix to checker.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:30:22 +0000