aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-03-27STM: refine the notion of "simply a tactic"Enrico Tassi
2015-03-27Properly handle extra "clean" targets with coq_makefile.Guillaume Melquiond
2015-03-27use a more compact representation of non-constant constructorsBenjamin Gregoire
2015-03-26allows the vm to deal with inductive type with 8388607 constant constructors ...Benjamin Gregoire
2015-03-26fix compilationBenjamin Gregoire
2015-03-26Fix bug 4157,Benjamin Gregoire
2015-03-26add coqdep in distributed_exec, else make does not work.Benjamin Gregoire
2015-03-26STM: change how proof mode switching commands are handled (decl_mode)Enrico Tassi
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-03-25More clever representation of substituted Cemitcode.Pierre-Marie Pédrot
2015-03-25Summary: fix code to detect functional values in summaryEnrico Tassi
2015-03-25STM: avoid processing asynchronously empty proofs (Close: #4134)Enrico Tassi
2015-03-25Exporting memory representation of STM tasks for votour.Pierre-Marie Pédrot
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-03-25Another example about the consequence of a wrong computation of theHugo Herbelin
2015-03-25Use kernel names instead of user names when looking for coercions. (Fix for b...Guillaume Melquiond
2015-03-25coqc: fix --helpEnrico Tassi
2015-03-25Correcting a bug introduced by universes polymorphismjforest
2015-03-25correcting a bug with aliased when using Functional Schemeforest
2015-03-24Updating test-suite (see previous commit).Hugo Herbelin
2015-03-24Fixing computation of non-recursively uniform arguments in theHugo Herbelin
2015-03-24Fixing wrong rel_context in checking positivity condition.Hugo Herbelin
2015-03-24Functorized interface over object representation in votour.Pierre-Marie Pédrot
2015-03-24Fixing representation of dynamics in votour (again).Pierre-Marie Pédrot
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-03-24Revert "Useless check when loading notations through import."Pierre-Marie Pédrot
2015-03-23Dedicated type for on-demand objects in Library.Pierre-Marie Pédrot
2015-03-23coqchk: more prints when -debugEnrico Tassi
2015-03-23Load: don't give anomaly on aborted proofs (Close: #3882)Enrico Tassi
2015-03-22Announcing * and ** which were not official yet in 8.4.Hugo Herbelin
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-03-22Aliasing give_up with admitEnrico Tassi
2015-03-22STM: if Set Universe Polymorphism then synchronous (#4119)Enrico Tassi
2015-03-22STM: do not delegate proofs containing PrintEnrico Tassi
2015-03-22STM: after every command restore the expected proof modeEnrico Tassi
2015-03-22typoEnrico Tassi
2015-03-21Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)Guillaume Melquiond
2015-03-21Avoid segfault from code extracted to ghc. (Fix for bug #1257)Guillaume Melquiond
2015-03-21Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Guillaume Melquiond
2015-03-21Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Guillaume Melquiond
2015-03-20Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.Pierre Courtieu
2015-03-18More sharing in module substitution.Pierre-Marie Pédrot
2015-03-18add -type-in-type to the usage messageDaniel R. Grayson
2015-03-18Fixing internal representation of Dyn.t in votour.Pierre-Marie Pédrot
2015-03-17Add function to fix the non-substituted universe variables of an evar_map.Matthieu Sozeau
2015-03-16Removing the whole library content from the summary.Pierre-Marie Pédrot
2015-03-16More invariants in Library.Pierre-Marie Pédrot
2015-03-16gitattributes: add `.mailmap` file to the list of files excluded from the `.t...Arnaud Spiwack
2015-03-16Gitattributes file added to generate archive.Guillaume Claret
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-20 08:45:14 +0000