aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-22Bugfix 3604 : more robust Unix.lockfFrédéric Besson
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-17Revert "Fixing a loop in proof reconstruction for congruence (#2447)."Hugo Herbelin
2014-10-17Fixing a loop in proof reconstruction for congruence (#2447).Hugo Herbelin
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-09Restoring plugins/xml/README erased by mistake.Hugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-06decl_mode: stay in declarative modeEnrico Tassi
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-10-01Fix cbn behavior wrt simpl no matchPierre Boutillier
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 10:29:56 +0000