aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-23Fix previous commit on extraction.Maxime Dénès
2015-01-23Extraction: fix #3629.Maxime Dénès
2015-01-12Derive -> derive occurencesPierre Boutillier
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-11Extraction: discard unnecessary code inside modules without signaturesPierre Letouzey
2015-01-11Extraction: no more ascii blob in type variables (fix #3227)Pierre Letouzey
2015-01-11Extraction : some more support functions for a future "Extraction Compute"Pierre Letouzey
2015-01-11Extraction: minor tweaks to ease ongoing experiments about LambdaPierre Letouzey
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:13:54 +0000