aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-03-04Uniformizing the parsing of argument scopes in Ltac.Pierre-Marie Pédrot
2016-03-04Merge pull request #97 from clarus/trunkPierre-Marie Pédrot
2016-02-29Merge branch 'clean-atomic-tactics'Pierre-Marie Pédrot
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "fix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-28Printing notations: Cleaning in anticipation of fixing #4592.Hugo Herbelin
2016-02-28Slightly contracting code of evarconv.ml.Hugo Herbelin
2016-02-27Removing Tacmach.New qualification in Tacinterp.Pierre-Marie Pédrot
2016-02-27Removing some compatibility layers in Tacinterp.Pierre-Marie Pédrot
2016-02-26Qcabs : absolute value on normalized rational numbers QcPierre Letouzey
2016-02-26Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)Pierre Letouzey
2016-02-26Qcanon : implement some old suggestions by C. AugerPierre Letouzey
2016-02-24Merge branch 'remove-quotations'Pierre-Marie Pédrot
2016-02-24Removing the METAIDENT token, as it is not used anymore.Pierre-Marie Pédrot
2016-02-24Removing the MetaIdArg entry of tactic expressions.Pierre-Marie Pédrot
2016-02-24Removing the Q_coqast module.Pierre-Marie Pédrot
2016-02-24Getting rid of the "<:tactic< ... >>" quotations.Pierre-Marie Pédrot
2016-02-23Moving tauto.ml4 to a proper ML file.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-20Fixing bug #4540: CoqIDE bottom progress bar does not update.Pierre-Marie Pédrot
2016-02-19Fix regression from 8.4 in reflexivity/...Matthieu Sozeau
2016-02-19Merge branch 'located-universes'Pierre-Marie Pédrot
2016-02-19Adding location to universes generated by the pretyper.Pierre-Marie Pédrot
2016-02-19Allowing to attach location to universes in UState.Pierre-Marie Pédrot
2016-02-19Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.Pierre-Marie Pédrot
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-02-19STM: Print/Extraction have to be skipped if -quickEnrico Tassi
2016-02-19CoqIDE: STOP button also stops workers (fix #4542)Enrico Tassi
2016-02-19STM: classify some variants of Instance as regular `Fork nodes.Enrico Tassi
2016-02-18FIX: of my previous merging mistakeMatej Kosik
2016-02-18ADD: Names.Name.is_{anonymous,name}Matej Kosik
2016-02-17Fixing the Proofview.Goal.goal function.Pierre-Marie Pédrot
2016-02-17Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Pierre-Marie Pédrot
2016-02-17CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-17CLEANUP: Renaming "Util.compose" function to "%"Matej Kosik
2016-02-16Tacticals: typo in a commentPierre Letouzey
2016-02-16Term: fix a comment (first de Bruijn index is 1)Pierre Letouzey
2016-02-16Renaming variants of Entries.local_entryMatej Kosik
2016-02-15CLEANUP: Simplifying the changes done in "checker/*"Matej Kosik
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-15CLEANUP: Simplifying the changes done in "kernel/*"Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 04:17:54 +0000