aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-09refman: switch all source files to utf8Pierre Letouzey
2014-12-09refman: fix broken urlsPierre Letouzey
2014-12-09refman: remove ?uri=referer in urls pointing to validator.w3.orgPierre Letouzey
2014-12-09refman/Omega.tex: do not advertize Pierre Cregut's email for bug reportsPierre Letouzey
2014-12-09refman/coqdoc.tex: fix two erroneous \urlPierre Letouzey
2014-12-09refman: for xhtml validity, add 'alt' attributes to imgPierre Letouzey
2014-12-09refman: avoid label names with whitespace (unsupported in html)Pierre Letouzey
2014-12-09refman: xhtml validity of the cover pagePierre Letouzey
2014-12-09coqdoc.css: fix a few errorsPierre Letouzey
2014-12-09coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 fro...Pierre Letouzey
2014-12-09doc/stdlib: fix the xhtml validity of the index-list templatePierre Letouzey
2014-12-09doc: improved xhtml compatibility (cover, header,...)Pierre Letouzey
2014-12-09doc/stdlib: fix the html charset in header.html and coPierre Letouzey
2014-12-09doc: version number in cover.html + updates in coq.inria.fr stylePierre Letouzey
2014-12-09Port to trunk commit r16062 of v8.4 (Correction des entĂȘtes pour la document...notin
2014-12-09Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat...notin
2014-12-08Fixing wrong evar_map in return clause inference, revealed by 48509b611.Hugo Herbelin
2014-12-08Improved criterion for evar restriction in the configurationHugo Herbelin
2014-12-08This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.Hugo Herbelin
2014-12-08Closing bug 3837Julien Forest
2014-12-08Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Arnaud Spiwack
2014-12-07Step 4 : atomize_thenHugo Herbelin
2014-12-07Step 2Hugo Herbelin
2014-12-07Step 1Hugo Herbelin
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-12-07Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE bu...Hugo Herbelin
2014-12-07Ensuring that ide_slave and stm receive only .v files from CoqIDE.Hugo Herbelin
2014-12-07Improving evar restriction (this is a risky change, as I remember aHugo Herbelin
2014-12-07Improved tracking of the origin of evars.Hugo Herbelin
2014-12-07Had forgotten some debugging printer.Hugo Herbelin
2014-12-07Exporting store of goals so that new_evar in convert, intro, etc. canHugo Herbelin
2014-12-07Removing import of Proofview in debugger because its module Goal hidesHugo Herbelin
2014-12-07Improving e11854569b8 on when to print goals in coqtop mode.Hugo Herbelin
2014-12-05More consistent printing of evars in evar_map debugging printer.Hugo Herbelin
2014-12-05Commits on evar-evar unification fixed HoTT_coq_106 and improved theHugo Herbelin
2014-12-05Fix debugger Tactic Unification.Hugo Herbelin
2014-12-05More printers in tracer.Hugo Herbelin
2014-12-05Small cleaning and uniformization in unification flags:Hugo Herbelin
2014-12-04Improving error message when one instance-hole is not found.Hugo Herbelin
2014-12-04New approach to deal with evar-evar unification problems in differentHugo Herbelin
2014-12-04Take benefit of improved name preservation of evars in e2fa65fcc.Hugo Herbelin
2014-12-04Trying a new policy for when to automatically print goals (grantingHugo Herbelin
2014-12-04Occur-check in refine.Arnaud Spiwack
2014-12-04Refine primitive: [unsafe] is now true by default.Arnaud Spiwack
2014-12-04Some refactoring following previous commit.Arnaud Spiwack
2014-12-04Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.Arnaud Spiwack
2014-12-04Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.Arnaud Spiwack
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-12-04coqdep: granting #2506 (./dir is the same as dir)Hugo Herbelin