aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/invfun.ml
AgeCommit message (Expand)Author
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15More conversion functions in the new tactic API.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-10-19Function debug mode more formatted.Pierre Courtieu
2015-10-02Univs: fix evar_map leaks bugs in FunctionMatthieu Sozeau
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-04-15Remove dirty debug printing from funind.Maxime Dénès
2015-04-14Function now supports puniveresjforest
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-12Passing some tactics to the new monad type.Pierre-Marie Pédrot
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-05-06Fix funind w.r.t. universesMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-24Rtree : cleanup of the comparing codeletouzey
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-30recdef: restore old semantics (pre STM)gareuselesinge
2013-08-30Fix typo in error messagegareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-10-31correcting a little bug in Functionjforest
2012-09-24Fixing a bug introduced in Funind plugin when reorganizing the CListppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:53:26 +0000