aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-07-22Minor cleaning.Maxime Dénès
2014-07-22Revert "Extend subterm relation to pattern matching in return predicates."Maxime Dénès
2014-07-22Revert "Propagate size info through pattern matching in predicates, for the"Maxime Dénès
2014-07-22Propagate size info through pattern matching in predicates, for theMaxime Dénès
2014-07-22Extend subterm relation to pattern matching in return predicates.Maxime Dénès
2014-07-22Fix check_inductive_codomain.Maxime Dénès
2014-07-22Refine check_is_subterm.Maxime Dénès
2014-07-22Refined guard condition of cofixpoints, to anticipate potential futurMaxime Dénès
2014-07-22First attempt at a fix for guard condition on cofixpoints.Maxime Dénès
2014-07-22Add test-suite file for guard condition on cofixpoints.Maxime Dénès
2014-07-22Typo in comment.Maxime Dénès
2014-07-22Simplified rect2, it turns out Arthur's trick was not required.Maxime Dénès
2014-07-22A version of Fin.rect2 that is compatible with the fix of the guard condition.Maxime Dénès
2014-07-22Fixed proof of irrelevance of le on nat, inspired by theMaxime Dénès
2014-07-22Made intersection on regular trees less intensional.Maxime Dénès
2014-07-22Refining match subterm and commutative cut rules. The parameters that areMaxime Dénès
2014-07-22Tentative fix for the commutative cut subterm rule.Maxime Dénès
2014-07-22Tentative patch for incompatibility between subterm relation and dependentMaxime Dénès
2014-07-22Ide: Drop argument added by MacOS during .app launchPierre Boutillier
2014-07-22the art of forgetting new files during rebase -iPierre Boutillier
2014-07-22A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundlePierre Boutillier
2014-07-22Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsPierre Boutillier
2014-07-22When I make MacOS binary, I would like to have a coqtop able to speak to coqi...Pierre Boutillier
2014-07-22Small code sharing in TacticMatching.Pierre-Marie Pédrot
2014-07-22Adding a "is_val" primitive to IStream.Pierre-Marie Pédrot
2014-07-21Universe level maps use HMaps.Pierre-Marie Pédrot
2014-07-21Missing primitives in HMap.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-18 08:34:39 +0000