aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
* refman: fix broken urlsGravatar Pierre Letouzey2014-12-09
* refman: remove ?uri=referer in urls pointing to validator.w3.orgGravatar Pierre Letouzey2014-12-09
* refman/Omega.tex: do not advertize Pierre Cregut's email for bug reportsGravatar Pierre Letouzey2014-12-09
* refman/coqdoc.tex: fix two erroneous \urlGravatar Pierre Letouzey2014-12-09
* refman: for xhtml validity, add 'alt' attributes to imgGravatar Pierre Letouzey2014-12-09
* refman: avoid label names with whitespace (unsupported in html)Gravatar Pierre Letouzey2014-12-09
* refman: xhtml validity of the cover pageGravatar Pierre Letouzey2014-12-09
* coqdoc.css: fix a few errorsGravatar Pierre Letouzey2014-12-09
* coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 fro...Gravatar Pierre Letouzey2014-12-09
* doc/stdlib: fix the xhtml validity of the index-list templateGravatar Pierre Letouzey2014-12-09
* doc: improved xhtml compatibility (cover, header,...)Gravatar Pierre Letouzey2014-12-09
* doc/stdlib: fix the html charset in header.html and coGravatar Pierre Letouzey2014-12-09
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-12-09
* Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la document...Gravatar notin2014-12-09
* Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat...Gravatar notin2014-12-09
* Fixing wrong evar_map in return clause inference, revealed by 48509b611.Gravatar Hugo Herbelin2014-12-08
* Improved criterion for evar restriction in the configurationGravatar Hugo Herbelin2014-12-08
* This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.Gravatar Hugo Herbelin2014-12-08
* Closing bug 3837Gravatar Julien Forest2014-12-08
* Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Gravatar Arnaud Spiwack2014-12-08
* Step 4 : atomize_thenGravatar Hugo Herbelin2014-12-07
* Step 2Gravatar Hugo Herbelin2014-12-07
* Step 1Gravatar Hugo Herbelin2014-12-07
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE bu...Gravatar Hugo Herbelin2014-12-07
* Ensuring that ide_slave and stm receive only .v files from CoqIDE.Gravatar Hugo Herbelin2014-12-07
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
* Had forgotten some debugging printer.Gravatar Hugo Herbelin2014-12-07
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
* Removing import of Proofview in debugger because its module Goal hidesGravatar Hugo Herbelin2014-12-07
* Improving e11854569b8 on when to print goals in coqtop mode.Gravatar Hugo Herbelin2014-12-07
* More consistent printing of evars in evar_map debugging printer.Gravatar Hugo Herbelin2014-12-05
* Commits on evar-evar unification fixed HoTT_coq_106 and improved theGravatar Hugo Herbelin2014-12-05
* Fix debugger Tactic Unification.Gravatar Hugo Herbelin2014-12-05
* More printers in tracer.Gravatar Hugo Herbelin2014-12-05
* Small cleaning and uniformization in unification flags:Gravatar Hugo Herbelin2014-12-05
* Improving error message when one instance-hole is not found.Gravatar Hugo Herbelin2014-12-04
* New approach to deal with evar-evar unification problems in differentGravatar Hugo Herbelin2014-12-04
* Take benefit of improved name preservation of evars in e2fa65fcc.Gravatar Hugo Herbelin2014-12-04
* Trying a new policy for when to automatically print goals (grantingGravatar Hugo Herbelin2014-12-04
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
* Refine primitive: [unsafe] is now true by default.Gravatar Arnaud Spiwack2014-12-04
* Some refactoring following previous commit.Gravatar Arnaud Spiwack2014-12-04
* Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.Gravatar Arnaud Spiwack2014-12-04
* Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.Gravatar Arnaud Spiwack2014-12-04
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* coqdep: granting #2506 (./dir is the same as dir)Gravatar Hugo Herbelin2014-12-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 02:58:03 +0000