aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-03-06Fix syntax highlighting of Extract Inductive.Guillaume Melquiond
2015-03-06Add syntax highlighting for Declare Module.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Import and Export.Guillaume Melquiond
2015-03-06Add syntax highlighting for Declare ML Module.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Require.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Scheme.Guillaume Melquiond
2015-03-06Do not highlight "using" as a constr keyword.Guillaume Melquiond
2015-03-06Add syntax highlighting for About.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Save.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context.Guillaume Melquiond
2015-03-06Add syntax highlighting for Coercion.Guillaume Melquiond
2015-03-06Fix syntax highlighting of "Require multiple libraries".Guillaume Melquiond
2015-03-06MMapPositive: another implementation of MMapsPierre Letouzey
2015-03-05Fix testsuite with respect to the new formatting of Fail messages.Guillaume Melquiond
2015-03-05Preprend Fail to all the expected failures in the documentation.Guillaume Melquiond
2015-03-05Do not prepend a "Error:" header when the error is expected by the user.Guillaume Melquiond
2015-03-05MMaps again : adding MMapList, an implementation by ordered listPierre Letouzey
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
2015-03-04Fix bug #3532, providing universe inconsistency information when aMatthieu Sozeau
2015-03-03Fix test-suite file, this is open.Matthieu Sozeau
2015-03-03Fix bug #3732: firstorder was using detyping to build existentialMatthieu Sozeau
2015-03-03Add missing test-suite files and update gitignore.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:29:20 +0000