aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-13Merge branch 'v8.5' into trunkArnaud Spiwack
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-11Merge branch 'v8.5'Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-19 03:30:43 +0000