aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-01Makefile.build : improved rules about .cm(x)aPierre Letouzey
2016-06-01Makefile.build : update the otags rulePierre Letouzey
2016-06-01g_tactics : remove opt_bindings (2-line dead code)Pierre Letouzey
2016-06-01Makefile.common : avoid warnings about files linked twicePierre Letouzey
2016-06-01Merge branch 'yet-another-makefile-bigbang' into trunkPierre Letouzey
2016-06-01Yet another Makefile reform : a unique phase without nasty make tricksPierre Letouzey
2016-06-01Makefile: restore the use of coqdep_boot for creating .v.d filesPierre Letouzey
2016-05-31This patch splits pretty printing representation from IO operations.Pierre-Marie Pédrot
2016-05-31Making the grammar/ folder independent from the other ones.Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2016-05-31Checker: no more -I kernel via a few symlinks (for Names and Esubst)Pierre Letouzey
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-26Update required OCaml version in configure.Maxime Dénès
2016-05-23typosEnrico Tassi
2016-05-20Extraction: code cleanup in CommonPierre Letouzey
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-19native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19adding "user-contrib" directory to ".gitignore"Matej Kosik
2016-05-19Unicode.ascii_of_ident is now truly injectivePierre Letouzey
2016-05-19Unicode.ascii_of_ident is now truly injectivePierre Letouzey
2016-05-19Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Pierre Letouzey
2016-05-17Putting all the tactics exported by the Tactics module in the new monad API.Pierre-Marie Pédrot
2016-05-17Removing some compatibility layers in Tactics.Pierre-Marie Pédrot
2016-05-17Removing the old refine tactic from the Tactics module.Pierre-Marie Pédrot
2016-05-17Put the "move" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "change" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "specialize_eq" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize dependent" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "*_cast_no_check" tactics in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact_constr" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-16Fix bug #4737: cycle tactic doesn't like zero goals.Pierre-Marie Pédrot
2016-05-16Generate more user-readable tactic notation kernel names.Pierre-Marie Pédrot
2016-05-16Merge pull request #170 from relrod/patch-1Pierre-Marie Pédrot
2016-05-15Fix a really small doc typoRicky Elrod
2016-05-14Removing unexcepted activation of option "Regular Subst Tactic", sinceHugo Herbelin
2016-05-14More hints on how to fix compatibility issues.Hugo Herbelin
2016-05-14Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.Pierre-Marie Pédrot
2016-05-13Dyn: simplify API introducing an Easy submoduleEnrico Tassi
2016-05-13More informative error message when interpreting ltac variables in terms.Pierre-Marie Pédrot
2016-05-12Small optimization in evar resolution.Pierre-Marie Pédrot
2016-05-12Fix bug #4722: Coq dies when encountering broken symbolic links.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:54:42 +0000