aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Pierre-Marie Pédrot
2016-01-17Exporting Genarg implementation in the API.Pierre-Marie Pédrot
2016-01-17Reimplementing Genarg safely.Pierre-Marie Pédrot
2016-01-17Adding a structure indexed by tags.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-17Removing dynamic entries from Pcoq.Pierre-Marie Pédrot
2016-01-17ML extensions use untyped representation of user entries.Pierre-Marie Pédrot
2016-01-16Separating the parsing of user-defined entries from their intepretation.Pierre-Marie Pédrot
2016-01-16Less type-unsafety in Pcoq.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2016-01-14Moving is_quantified_hypothesis to new proof engine.Hugo Herbelin
2016-01-14Updating and improving the documentation of intros patterns.Hugo Herbelin
2016-01-14Continuing 003fe3d5e on parsing positions.Hugo Herbelin
2016-01-14Changing "P is assumed" to "P is declared".Hugo Herbelin
2016-01-14Update in the documentation of parts of the code of destruct/induction.Hugo Herbelin
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13Fixing success of test for #3848 after move to directory "closed".Hugo Herbelin
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-12Fixing #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2016-01-12Fixing #4256 and #4484 (changes in evar-evar resolution made that newHugo Herbelin
2016-01-12Reporting about the new tactical unshelve.Hugo Herbelin
2016-01-12Extend last commit: keyed unification uses full conversions on the applied co...Matthieu Sozeau
2016-01-12Extend Keyed Unification tests with the one from R. Krebbers.Matthieu Sozeau
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-12Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Hugo Herbelin
2016-01-12Documenting dtauto and dintuition.Hugo Herbelin
2016-01-12Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Hugo Herbelin
2016-01-12Documenting option 'Set Bracketing Last Introduction Pattern'.Hugo Herbelin
2016-01-12restore documentation of admitEnrico Tassi
2016-01-11CLEANUP: removing unnecessary wrapperMatej Kosik
2016-01-11COMMENTS: added to the "Constrexpr.CCases" variant.Matej Kosik
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-11Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Matthieu Sozeau
2016-01-11COMMENTS: of "Constr.case_info" type were updated.Matej Kosik
2016-01-11COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Matej Kosik
2016-01-09Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.Pierre-Marie Pédrot
2016-01-08Monotonizing Ftactic.Pierre-Marie Pédrot
2016-01-08Be more verbose about failure to compile libraries to native code.Guillaume Melquiond
2016-01-07Fix a misleading comment for substn_varsMatthieu Sozeau
2016-01-07Fix bug #4480: progress was not checked for setoid_rewrite.Matthieu Sozeau
2016-01-06Fix description of command-line options in the manual.Guillaume Melquiond
2016-01-06Remove deprecated command-line options such as "-as".Guillaume Melquiond
2016-01-06Make code more readable by not mixing list traversal and option processing.Guillaume Melquiond
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Prevent coq_makefile from parsing project files in the reverse order. (Fix bu...Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 09:11:09 +0000