aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Removing a warning in CoqOps.Gravatar Pierre-Marie Pédrot2015-09-15
* Test for bug #4269.Gravatar Pierre-Marie Pédrot2015-09-15
* Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.Gravatar Pierre-Marie Pédrot2015-09-15
* STM: Reset takes Ltac <ident> into account (Close #4316)Gravatar Enrico Tassi2015-09-15
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Fixing bug #2498: Coqide navigation preferences delayed effect.Gravatar Pierre-Marie Pédrot2015-09-12
* typo in refman.Gravatar Pierre Courtieu2015-09-10
* Fixing previous patch.Gravatar Pierre-Marie Pédrot2015-09-10
* Fixing the XML lexer definition of names to match the standard.Gravatar Pierre-Marie Pédrot2015-09-10
* Extending the grammar for CoqIDE preferences so as to match trunk.Gravatar Pierre-Marie Pédrot2015-09-10
* Emphasizing that eta for vectors is an instance of caseS, as pointedGravatar Hugo Herbelin2015-09-08
* Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsGravatar Hugo Herbelin2015-09-08
* Minor modifications to WeakFanTheorem.Gravatar Hugo Herbelin2015-09-08
* Ensuring that patterns of the form pat/constr move the hypotheses replacingGravatar Hugo Herbelin2015-09-08
* Short cosmetic changes in tactics.ml.Gravatar Hugo Herbelin2015-09-08
* A bit of documentation of OCaml code for intro_patterns.Gravatar Hugo Herbelin2015-09-08
* New option "Unset Bracketing Last Introduction Pattern" for preservingGravatar Hugo Herbelin2015-09-08
* Fixing clearing of temporary hypotheses with intro pattern pat/constr.Gravatar Hugo Herbelin2015-09-08
* Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedGravatar Hugo Herbelin2015-09-08
* Hacking parser so as to support both [> ... ] and [id].Gravatar Hugo Herbelin2015-09-08
* Adding a proof of eta on Vector.t of non-zero size.Gravatar Hugo Herbelin2015-09-08
* Documenting the code when preference is given to expansion of defaultGravatar Hugo Herbelin2015-09-08
* Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Gravatar Maxime Dénès2015-09-06
* Fixed critical bug in 31 bit arithmetic of VMGravatar Catalin Hritcu2015-09-06
* Adding a Makefile target for the MSets and MMaps directories.Gravatar Pierre-Marie Pédrot2015-09-06
* Update test-suite after 518049fe7.Gravatar Maxime Dénès2015-09-03
* print universes when dumping bytecode.Gravatar Gregory Malecha2015-09-03
* Improve directives for Haskell extraction of nat.Gravatar Maxime Dénès2015-09-03
* Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.vGravatar Nickolai Zeldovich2015-09-03
* Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.vGravatar Nickolai Zeldovich2015-09-03
* Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
* Also there's an extra space in the error message.Gravatar mlasson2015-09-03
* Add an if_verbose for "Fetching opaque proofs ..."Gravatar mlasson2015-09-03
* Missing argument "-c" for coqdep in coq_makefileGravatar mlasson2015-09-03
* STM: save a full state for queries.Gravatar Enrico Tassi2015-09-01
* Code cleaning in Obligations.Gravatar Pierre-Marie Pédrot2015-08-22
* Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Gravatar Hugo Herbelin2015-08-21
* Removing code duplication in Lemmas.Gravatar Pierre-Marie Pédrot2015-08-19
* Documentation by giving a name to a large type.Gravatar Pierre-Marie Pédrot2015-08-19
* Highlighting of the "Next Obligation" command in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-17
* windows build scripts made more accurate in detecting failuresGravatar Enrico Tassi2015-08-17
* Remove duplicate code.Gravatar Guillaume Melquiond2015-08-17
* Remove generatable documentation files from repository. (Fix bug #4315)Gravatar Guillaume Melquiond2015-08-17
* Revert the four previous commits and update the description of Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
* More invariants in Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
* More parametric type for generalized XML.Gravatar Pierre-Marie Pédrot2015-08-15
* Statically ensure that we omit null annotations in Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
* Fixing richpp behaviour w.r.t. its specification.Gravatar Pierre-Marie Pédrot2015-08-15
* report the full module path when reporting errors in coqdepGravatar Gregory Malecha2015-08-13
* Test file for #4254: Mutual inductives with parameters on Type raises anomaly.Gravatar Maxime Dénès2015-08-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 10:05:22 +0000