aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/invfun.ml
AgeCommit message (Expand)Author
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 03:55:56 +0000