aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* CoqIDE: fix tag colors to support superposing unsafe and partialGravatar Enrico Tassi2015-03-11
* CoqIDE: restore module/proof name in info barGravatar Enrico Tassi2015-03-11
* CoqIDE: do not lose tag on Qed ending focused proofGravatar Enrico Tassi2015-03-11
* STM: ease re-editing of Admitted proofsGravatar Enrico Tassi2015-03-11
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Do not display the status of monomorphic constants unless in universe-polymor...Gravatar Guillaume Melquiond2015-03-09
* Test for bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
* Fixing bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
* Test for #4035 (dependent destruction from Ltac).Gravatar Hugo Herbelin2015-03-07
* Reverting r10021 which enforces early assumptions on freshness whichGravatar Hugo Herbelin2015-03-07
* Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Gravatar Hugo Herbelin2015-03-07
* Add some missing Proof keywords.Gravatar Guillaume Melquiond2015-03-06
* Simplify grammar for syntax highlighting by removing extraneous parentheses.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Print/Reset Extraction.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Extraction Inline and add Separate Extraction.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Extraction Language.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Typeclasses Opaque.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Module (Type).Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Extract Inductive.Gravatar Guillaume Melquiond2015-03-06
* Add syntax highlighting for Declare Module.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Import and Export.Gravatar Guillaume Melquiond2015-03-06
* Add syntax highlighting for Declare ML Module.Gravatar Guillaume Melquiond2015-03-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 17:45:37 +0000