aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix handling of universes at the end of proofs, esp. for async proof processing.Gravatar Matthieu Sozeau2014-07-25
* 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
* 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
* 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
* Revert "Adding a "is_val" primitive to IStream."Gravatar Pierre-Marie Pédrot2014-07-24
* fixup fakeide test-suiteGravatar Pierre Boutillier2014-07-24
* Make MacStore like coqide moreGravatar Pierre Boutillier2014-07-24
* 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
* When closing a proof, make sure that the types have their evar substituted.Gravatar Arnaud Spiwack2014-07-23
* 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 te...Gravatar Arnaud Spiwack2014-07-23
* Change the interface of proof_global to take an evar_map instead of a univers...Gravatar Arnaud Spiwack2014-07-23
* 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
* Revert "Propagate size info through pattern matching in predicates, for the"Gravatar Maxime Dénès2014-07-22
* Propagate size info through pattern matching in predicates, for theGravatar Maxime Dénès2014-07-22
* Extend subterm relation to pattern matching in return predicates.Gravatar Maxime Dénès2014-07-22
* Fix check_inductive_codomain.Gravatar Maxime Dénès2014-07-22
* Refine check_is_subterm.Gravatar Maxime Dénès2014-07-22
* Refined guard condition of cofixpoints, to anticipate potential futurGravatar Maxime Dénès2014-07-22
* 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
* A version of Fin.rect2 that is compatible with the fix of the guard condition.Gravatar Maxime Dénès2014-07-22
* Fixed proof of irrelevance of le on nat, inspired by theGravatar Maxime Dénès2014-07-22
* 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
* Tentative fix for the commutative cut subterm rule.Gravatar Maxime Dénès2014-07-22
* Tentative patch for incompatibility between subterm relation and dependentGravatar Maxime Dénès2014-07-22
* 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
* A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundleGravatar Pierre Boutillier2014-07-22
* Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsGravatar Pierre Boutillier2014-07-22
* When I make MacOS binary, I would like to have a coqtop able to speak to coqi...Gravatar Pierre Boutillier2014-07-22
* Small code sharing in TacticMatching.Gravatar Pierre-Marie Pédrot2014-07-22
* Adding a "is_val" primitive to IStream.Gravatar Pierre-Marie Pédrot2014-07-22
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
* Missing primitives in HMap.Gravatar Pierre-Marie Pédrot2014-07-21
* Fixing semantics of HSet.inter and HSet.diff.Gravatar Pierre-Marie Pédrot2014-07-21
* More straightforward definition of Universes.add_list_map.Gravatar Pierre-Marie Pédrot2014-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-17 17:03:16 +0000