aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-05Using build_selector from Equality as a replacement of the selectorHugo Herbelin
2016-03-05Exporting build_selector, a component of discriminate, for use in congruence.Hugo Herbelin
2016-03-05Generalizing the uses of tactic scopes everywhere.Pierre-Marie Pédrot
2016-03-05Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Pierre-Marie Pédrot
2016-03-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime Dénès
2016-03-04Adding some standard arguments in tactic scopes.Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-03-04All arguments defined through ARGUMENT EXTEND declare a tactic scope.Pierre-Marie Pédrot
2016-03-04Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Pierre-Marie Pédrot
2016-03-04Exchanging roles of tactic_arg and tactic_top_or_arg entries.Pierre-Marie Pédrot
2016-03-04Removing the UConstr entry of the tactic_arg AST.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
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-03-04Fix a typo in dev/doc/changes.txtJason Gross
2016-03-03Adding a test for the behaviour of open_constr described in #3777.Pierre-Marie Pédrot
2016-03-03Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Pierre-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-28Fixing bug #4596: [rewrite] broke in the past few weeks.Pierre-Marie Pédrot
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-24Document Hint Mode, cleanup Hint doc.Matthieu Sozeau
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-23Document differences of Hint Resolve and Hint ExternMatthieu Sozeau
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
2016-02-23Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Matthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 04:03:04 +0000