| Age | Commit message (Expand) | Author |
|---|
| 2014-12-09 | coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 fro... | Pierre Letouzey |
| 2014-12-09 | doc/stdlib: fix the xhtml validity of the index-list template | Pierre Letouzey |
| 2014-12-09 | doc: improved xhtml compatibility (cover, header,...) | Pierre Letouzey |
| 2014-12-09 | doc/stdlib: fix the html charset in header.html and co | Pierre Letouzey |
| 2014-12-09 | doc: version number in cover.html + updates in coq.inria.fr style | Pierre Letouzey |
| 2014-12-09 | Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la document... | notin |
| 2014-12-09 | Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat... | notin |
| 2014-12-08 | Fixing wrong evar_map in return clause inference, revealed by 48509b611. | Hugo Herbelin |
| 2014-12-08 | Improved criterion for evar restriction in the configuration | Hugo Herbelin |
| 2014-12-08 | This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e. | Hugo Herbelin |
| 2014-12-08 | Closing bug 3837 | Julien Forest |
| 2014-12-08 | Constructor tactics backtracking is done using [Tacticals.New] rather than [P... | Arnaud Spiwack |
| 2014-12-07 | Step 4 : atomize_then | Hugo Herbelin |
| 2014-12-07 | Step 2 | Hugo Herbelin |
| 2014-12-07 | Step 1 | Hugo Herbelin |
| 2014-12-07 | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin |
| 2014-12-07 | Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE bu... | Hugo Herbelin |
| 2014-12-07 | Ensuring that ide_slave and stm receive only .v files from CoqIDE. | Hugo Herbelin |
| 2014-12-07 | Improving evar restriction (this is a risky change, as I remember a | Hugo Herbelin |
| 2014-12-07 | Improved tracking of the origin of evars. | Hugo Herbelin |
| 2014-12-07 | Had forgotten some debugging printer. | Hugo Herbelin |
| 2014-12-07 | Exporting store of goals so that new_evar in convert, intro, etc. can | Hugo Herbelin |
| 2014-12-07 | Removing import of Proofview in debugger because its module Goal hides | Hugo Herbelin |
| 2014-12-07 | Improving e11854569b8 on when to print goals in coqtop mode. | Hugo Herbelin |
| 2014-12-05 | More consistent printing of evars in evar_map debugging printer. | Hugo Herbelin |
| 2014-12-05 | Commits on evar-evar unification fixed HoTT_coq_106 and improved the | Hugo Herbelin |
| 2014-12-05 | Fix debugger Tactic Unification. | Hugo Herbelin |
| 2014-12-05 | More printers in tracer. | Hugo Herbelin |
| 2014-12-05 | Small cleaning and uniformization in unification flags: | Hugo Herbelin |
| 2014-12-04 | Improving error message when one instance-hole is not found. | Hugo Herbelin |
| 2014-12-04 | New approach to deal with evar-evar unification problems in different | Hugo Herbelin |
| 2014-12-04 | Take benefit of improved name preservation of evars in e2fa65fcc. | Hugo Herbelin |
| 2014-12-04 | Trying a new policy for when to automatically print goals (granting | Hugo Herbelin |
| 2014-12-04 | Occur-check in refine. | Arnaud Spiwack |
| 2014-12-04 | Refine primitive: [unsafe] is now true by default. | Arnaud Spiwack |
| 2014-12-04 | Some refactoring following previous commit. | Arnaud Spiwack |
| 2014-12-04 | Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35. | Arnaud Spiwack |
| 2014-12-04 | Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075. | Arnaud Spiwack |
| 2014-12-04 | Reactivating option "Set Printing Existential Instances" for asking printing ... | Hugo Herbelin |
| 2014-12-04 | coqdep: granting #2506 (./dir is the same as dir) | Hugo Herbelin |
| 2014-12-04 | coqdep: Warning about ml file clashes, keeping the file corresponding | Hugo Herbelin |
| 2014-12-03 | Slight improving of a unification error message. | Hugo Herbelin |
| 2014-12-03 | Updading test-suite. | Hugo Herbelin |
| 2014-12-03 | In solve_evar_evar, orient the heuristic over arities with different | Hugo Herbelin |
| 2014-12-02 | When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if | Hugo Herbelin |
| 2014-12-02 | Postponing the "evar <= evar" problems instead of solving them in an | Hugo Herbelin |
| 2014-12-02 | Being more scrupulous on preserving subtyping in evar-evar problems. | Hugo Herbelin |
| 2014-12-02 | Being consistent in making arbitrary choices in recursive calls to | Hugo Herbelin |
| 2014-12-02 | Resolution of evar/evar problems: removed a test which should be | Hugo Herbelin |
| 2014-12-02 | For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota | Pierre-Marie Pédrot |
