aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-03-16Adding a primitive to dump the current association table of dynamic types.Pierre-Marie Pédrot
2015-03-15STM: -debug: better explanation of why not async (#4125)Enrico Tassi
2015-03-15STM: -quick: async no Proof using but no Section (#4124)Enrico Tassi
2015-03-14End of Bug 3986 - make cleanall removes .*.aux filesPierre Boutillier
2015-03-14Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warningPierre Boutillier
2015-03-14Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesignPierre Boutillier
2015-03-13Fix compilation with forthcoming Ocaml version 4.03.Arnaud Spiwack
2015-03-13Declarative mode: make it so that unfocussing can only be done for closed sub...Arnaud Spiwack
2015-03-13Declarative mode: remove dead code.Arnaud Spiwack
2015-03-13Declarative mode: remove a superfluous [set_proof_mode].Arnaud Spiwack
2015-03-13Declarative mode: fix the focus behaviour.Arnaud Spiwack
2015-03-13rewiring Czar printers that were disabledPierre Corbineau
2015-03-13CHANGES: more correct equivalent to "constructor tac" syntax.Arnaud Spiwack
2015-03-13Add some tests for tryifJason Gross
2015-03-13Fixing #4127 (command for locating exists notation in refman changed).Hugo Herbelin
2015-03-12Fixing bug #4055.Pierre-Marie Pédrot
2015-03-11Fix double print in decl_mode.Enrico Tassi
2015-03-11Fix regression in HoTT_coq_014.vEnrico Tassi
2015-03-11CoqIDE: load first _CoqProject file found and notify the userEnrico Tassi
2015-03-11CoqIDE: fix tag colors to support superposing unsafe and partialEnrico Tassi
2015-03-11CoqIDE: restore module/proof name in info barEnrico Tassi
2015-03-11CoqIDE: do not lose tag on Qed ending focused proofEnrico Tassi
2015-03-11STM: ease re-editing of Admitted proofsEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 17:33:34 +0000