aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* grammar: export constr_evalGravatar Enrico Tassi2015-03-30
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
* camlp4: grep away warnings in output/* testsGravatar Enrico Tassi2015-03-30
* coq_makefile: fix compilation with camlp4Gravatar Enrico Tassi2015-03-30
* fix code and bound for SWITCH instruction.Gravatar Benjamin Gregoire2015-03-30
* Ensuring more invariants in Constr_matching.Gravatar Pierre-Marie Pédrot2015-03-29
* Adding test for bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Fixing bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Normalize scope names before storing them in vo files. (Fix for bug #4162)Gravatar Guillaume Melquiond2015-03-27
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* STM: refine the notion of "simply a tactic"Gravatar Enrico Tassi2015-03-27
* Properly handle extra "clean" targets with coq_makefile.Gravatar Guillaume Melquiond2015-03-27
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
* allows the vm to deal with inductive type with 8388607 constant constructors ...Gravatar Benjamin Gregoire2015-03-26
* fix compilationGravatar Benjamin Gregoire2015-03-26
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
* add coqdep in distributed_exec, else make does not work.Gravatar Benjamin Gregoire2015-03-26
* STM: change how proof mode switching commands are handled (decl_mode)Gravatar Enrico Tassi2015-03-26
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* More clever representation of substituted Cemitcode.Gravatar Pierre-Marie Pédrot2015-03-25
* Summary: fix code to detect functional values in summaryGravatar Enrico Tassi2015-03-25
* STM: avoid processing asynchronously empty proofs (Close: #4134)Gravatar Enrico Tassi2015-03-25
* Exporting memory representation of STM tasks for votour.Gravatar Pierre-Marie Pédrot2015-03-25
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Another example about the consequence of a wrong computation of theGravatar Hugo Herbelin2015-03-25
* Use kernel names instead of user names when looking for coercions. (Fix for b...Gravatar Guillaume Melquiond2015-03-25
* coqc: fix --helpGravatar Enrico Tassi2015-03-25
* Correcting a bug introduced by universes polymorphismGravatar jforest2015-03-25
* correcting a bug with aliased when using Functional SchemeGravatar forest2015-03-25
* Updating test-suite (see previous commit).Gravatar Hugo Herbelin2015-03-24
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* Functorized interface over object representation in votour.Gravatar Pierre-Marie Pédrot2015-03-24
* Fixing representation of dynamics in votour (again).Gravatar Pierre-Marie Pédrot2015-03-24
* Fixing equality of notation_constrs. Fixes bug #4136.Gravatar Pierre-Marie Pédrot2015-03-24
* Revert "Useless check when loading notations through import."Gravatar Pierre-Marie Pédrot2015-03-24
* Dedicated type for on-demand objects in Library.Gravatar Pierre-Marie Pédrot2015-03-23
* coqchk: more prints when -debugGravatar Enrico Tassi2015-03-23
* Load: don't give anomaly on aborted proofs (Close: #3882)Gravatar Enrico Tassi2015-03-23
* Announcing * and ** which were not official yet in 8.4.Gravatar Hugo Herbelin2015-03-22
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* Aliasing give_up with admitGravatar Enrico Tassi2015-03-22
* STM: if Set Universe Polymorphism then synchronous (#4119)Gravatar Enrico Tassi2015-03-22
* STM: do not delegate proofs containing PrintGravatar Enrico Tassi2015-03-22
* STM: after every command restore the expected proof modeGravatar Enrico Tassi2015-03-22
* typoGravatar Enrico Tassi2015-03-22
* Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)Gravatar Guillaume Melquiond2015-03-21
* Avoid segfault from code extracted to ghc. (Fix for bug #1257)Gravatar Guillaume Melquiond2015-03-21
* Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Gravatar Guillaume Melquiond2015-03-21
* Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Gravatar Guillaume Melquiond2015-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 14:56:51 +0000