aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-11handling Functional Scheme for required but not imported modulesJulien Forest
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-08Closing bug 3837Julien Forest
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-11-25Fix order of arguments in Extract Constant for Pos.compare_cont.Maxime Dénès
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-07Fixing Functional Induction when applied to an alias (reference manualHugo Herbelin
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-05Writing the raw introduction tactic in the new monad.Pierre-Marie Pédrot
2014-11-03Writing rename_hyps in the new monad.Pierre-Marie Pédrot
2014-11-01Don't raise an error when printing intro-patterns in [functional induction].Arnaud Spiwack
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-28Haskell extraction: use explicit -XMagicHash instead of -fglasgow-extsNickolai Zeldovich
2014-10-28Haskell extraction: put unsafeCoerce type declaration laterNickolai Zeldovich
2014-10-27Removing an Evd.merge in Newring.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:40:32 +0000