aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2014-09-25Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",Xavier Clerc
2014-09-25Remove some 'deprecated' warnings.Xavier Clerc
2014-09-22Correction of error message (bug 3359)Julien Forest
2014-09-22Fixing bug 3951Julien Forest
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-12Discontinued xml plugin: improve the README.Arnaud Spiwack
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-05Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
2014-09-04Remove [Infer] option of records.Arnaud Spiwack
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Clean up a comment in plugins/romega/ReflOmegaCoreJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-25Correct a spelling mistakeJason Gross
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-12A couple of fixes/improvements in -beautify, but backtracking onHugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-08-05More proofs independent of the names generated by induction/elim overHugo Herbelin
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05Ring: prevent an error message to show in case of success.Arnaud Spiwack
2014-08-05Better fix of e5c025Pierre Boutillier
2014-08-04STM: VtQuery holds the id of the state it refers toCarst Tankink
2014-08-03Fix to make Coq compile, I think this should still be accepted.Matthieu Sozeau
2014-08-02Better struture for Ltac internalization environments in Constrintern.Pierre-Marie Pédrot
2014-08-01micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Frédéric Besson
2014-08-01Compatibility for compilation with ocaml 3.12 (at least).Hugo Herbelin
2014-08-01micromega : improve efficiency/termination of type-checkingFrédéric Besson
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-08-01Removing some tactic compatibility layer.Pierre-Marie Pédrot
2014-07-31micromega : refification recognises @eq T for T convertible with Z or RFrédéric Besson
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-07-23Derive plugin: add some comments.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 03:50:06 +0000