aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-04-27Revert "Fixing printing of Function."Hugo Herbelin
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
2016-04-27Fixing a mispelling coma -> comma.Hugo Herbelin
2016-04-27Fixing printing of Function.Hugo Herbelin
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Adding a universe argument to Pcoq.create_generic_entry.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
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-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
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
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-28Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Pierre-Marie Pédrot
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-18Fix a bug preventing the generation of graphs when doing multipleMatthieu Sozeau
2015-10-29Monotonizing Tactics.change_arg.Pierre-Marie Pédrot
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-28Do not pause globing in funind. (Fix bug #4382)Guillaume Melquiond
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-10-19Function debug mode more formatted.Pierre Courtieu
2015-10-19Partly fixes #3225. Removed some old experimental stuff in funind.Pierre Courtieu
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs: fix evar_map leaks bugs in FunctionMatthieu Sozeau
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:28:45 +0000