| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-12-01 | More invariants in the code of Rewrite. | Pierre-Marie Pédrot |
| 2014-12-01 | Fixing test-suite. | Pierre-Marie Pédrot |
| 2014-12-01 | Added an arithmetical characterization of the hypothesis of WKL. | Hugo Herbelin |
| 2014-12-01 | Remove dead code | Enrico Tassi |
| 2014-12-01 | Better comment | Enrico Tassi |
| 2014-11-30 | Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ... | Hugo Herbelin |
| 2014-11-30 | Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too. | Hugo Herbelin |
| 2014-11-30 | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot |
| 2014-11-30 | Adding a Refine Instance Mode option that allows to deactivate the | Pierre-Marie Pédrot |
| 2014-11-30 | Adding test for bug #3417. | Pierre-Marie Pédrot |
| 2014-11-30 | Test for bug #3485. | Pierre-Marie Pédrot |
| 2014-11-30 | Fixing printing of dirpathes in Ppconstr. It was reversed. | Pierre-Marie Pédrot |
| 2014-11-30 | Test for bug #3487. | Pierre-Marie Pédrot |
| 2014-11-30 | Test of bug #3682. | Pierre-Marie Pédrot |
| 2014-11-30 | Fixing bug #3682. | Pierre-Marie Pédrot |
