aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
* Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
* Fixing pop_rel_context.Gravatar Hugo Herbelin2015-08-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Hconsing continuedGravatar Hugo Herbelin2015-08-02
* Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
* Fixing pop_rel_contextGravatar Hugo Herbelin2015-08-02
* Documenting in passing.Gravatar Hugo Herbelin2015-08-02
* Hopefully clearer printing of stack when debugging evarconv unification.Gravatar Hugo Herbelin2015-08-02
* Failing when reaching end of file with unterminated comment whenGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
* Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
* Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
* Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-08-02
* Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* Documenting change of behavior of apply when the lemma is a tuple andGravatar Hugo Herbelin2015-08-02
* For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 03:22:05 +0000