aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.Gravatar Pierre Courtieu2015-03-20
* More sharing in module substitution.Gravatar Pierre-Marie Pédrot2015-03-18
* add -type-in-type to the usage messageGravatar Daniel R. Grayson2015-03-18
* Fixing internal representation of Dyn.t in votour.Gravatar Pierre-Marie Pédrot2015-03-18
* Add function to fix the non-substituted universe variables of an evar_map.Gravatar Matthieu Sozeau2015-03-17
* Removing the whole library content from the summary.Gravatar Pierre-Marie Pédrot2015-03-16
* More invariants in Library.Gravatar Pierre-Marie Pédrot2015-03-16
* gitattributes: add `.mailmap` file to the list of files excluded from the `.t...Gravatar Arnaud Spiwack2015-03-16
* Gitattributes file added to generate archive.Gravatar Guillaume Claret2015-03-16
* Adding a primitive to dump the current association table of dynamic types.Gravatar Pierre-Marie Pédrot2015-03-16
* STM: -debug: better explanation of why not async (#4125)Gravatar Enrico Tassi2015-03-15
* STM: -quick: async no Proof using but no Section (#4124)Gravatar Enrico Tassi2015-03-15
* End of Bug 3986 - make cleanall removes .*.aux filesGravatar Pierre Boutillier2015-03-14
* Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warningGravatar Pierre Boutillier2015-03-14
* Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesignGravatar Pierre Boutillier2015-03-14
* Fix compilation with forthcoming Ocaml version 4.03.Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: make it so that unfocussing can only be done for closed sub...Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: remove dead code.Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: remove a superfluous [set_proof_mode].Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: fix the focus behaviour.Gravatar Arnaud Spiwack2015-03-13
* rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-13
* CHANGES: more correct equivalent to "constructor tac" syntax.Gravatar Arnaud Spiwack2015-03-13
* Add some tests for tryifGravatar Jason Gross2015-03-13
* Fixing #4127 (command for locating exists notation in refman changed).Gravatar Hugo Herbelin2015-03-13
* Fixing bug #4055.Gravatar Pierre-Marie Pédrot2015-03-12
* Fix double print in decl_mode.Gravatar Enrico Tassi2015-03-11
* Fix regression in HoTT_coq_014.vGravatar Enrico Tassi2015-03-11
* CoqIDE: load first _CoqProject file found and notify the userGravatar Enrico Tassi2015-03-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 13:50:11 +0000