aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-12-04coqdep: Warning about ml file clashes, keeping the file correspondingHugo Herbelin
2014-12-03Slight improving of a unification error message.Hugo Herbelin
2014-12-03Updading test-suite.Hugo Herbelin
2014-12-03In solve_evar_evar, orient the heuristic over arities with differentHugo Herbelin
2014-12-02When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifHugo Herbelin
2014-12-02Postponing the "evar <= evar" problems instead of solving them in anHugo Herbelin
2014-12-02Being more scrupulous on preserving subtyping in evar-evar problems.Hugo Herbelin
2014-12-02Being consistent in making arbitrary choices in recursive calls toHugo Herbelin
2014-12-02Resolution of evar/evar problems: removed a test which should beHugo Herbelin
2014-12-02For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaPierre-Marie Pédrot
2014-12-01More invariants in the code of Rewrite.Pierre-Marie Pédrot
2014-12-01Fixing test-suite.Pierre-Marie Pédrot
2014-12-01Added an arithmetical characterization of the hypothesis of WKL.Hugo Herbelin
2014-12-01Remove dead codeEnrico Tassi
2014-12-01Better commentEnrico Tassi
2014-11-30Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...Hugo Herbelin
2014-11-30Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Hugo Herbelin
2014-11-30Documenting the Set Refine Instance Mode.Pierre-Marie Pédrot
2014-11-30Adding a Refine Instance Mode option that allows to deactivate thePierre-Marie Pédrot
2014-11-30Adding test for bug #3417.Pierre-Marie Pédrot
2014-11-30Test for bug #3485.Pierre-Marie Pédrot
2014-11-30Fixing printing of dirpathes in Ppconstr. It was reversed.Pierre-Marie Pédrot
2014-11-30Test for bug #3487.Pierre-Marie Pédrot
2014-11-30Test of bug #3682.Pierre-Marie Pédrot
2014-11-30Fixing bug #3682.Pierre-Marie Pédrot
2014-11-30Adding missing unsafe primitives to Proofview.Pierre-Marie Pédrot
2014-11-28fix compilation on ocaml 3.12 (Close: 3833)Enrico Tassi
2014-11-28Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.Arnaud Spiwack
2014-11-28Tactic primitives: missing [advance] lead to spurious dangling goals.Arnaud Spiwack
2014-11-28STM: if a-p-always-delegate fetch states from parked worker on edit-atEnrico Tassi
2014-11-28Future: API for blocking futuresEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 06:10:41 +0000