aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-09Do not display the status of monomorphic constants unless in universe-polymor...Guillaume Melquiond
2015-03-08Test for bug #2951.Pierre-Marie Pédrot
2015-03-08Fixing bug #2951.Pierre-Marie Pédrot
2015-03-07Test for #4035 (dependent destruction from Ltac).Hugo Herbelin
2015-03-07Reverting r10021 which enforces early assumptions on freshness whichHugo Herbelin
2015-03-07Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Hugo Herbelin
2015-03-06Add some missing Proof keywords.Guillaume Melquiond
2015-03-06Simplify grammar for syntax highlighting by removing extraneous parentheses.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Print/Reset Extraction.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Extraction Inline and add Separate Extraction.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Extraction Language.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Typeclasses Opaque.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Module (Type).Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-10 16:04:16 +0000