aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-03-14Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-13Adopting the same rules for interpreting @, abbreviations andHugo Herbelin
2016-03-13Adding a few functions on type union.Hugo Herbelin
2016-03-13Adding a file summarizing the inconsistencies in interpreting implicitHugo Herbelin
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-03-12Removing an empty file detected by Luc Grateau.Hugo Herbelin
2016-03-10Removing OCaml deprecated function names from the Lazy module.Pierre-Marie Pédrot
2016-03-09Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspi...Hugo Herbelin
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Fix test-suite file coq-prog-argsMatthieu Sozeau
2016-03-09Redo fix init_setoid -> init_relation_classesMatthieu Sozeau
2016-03-09Fixed bug #4533 with previous Keyed Unification commitMatthieu Sozeau
2016-03-09Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)Enrico Tassi
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-07Adding backtraces to scheme error messages.Pierre-Marie Pédrot
2016-03-07Re-enable OCaml warnings disabled by mistake as part of e759333.Maxime Dénès
2016-03-06Partial disentangling of Ltac codebase.Pierre-Marie Pédrot
2016-03-06Expurging grammar.mllib from uselessly linked modules.Pierre-Marie Pédrot
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-03-06Putting Tactic_debug just below Tacinterp.Pierre-Marie Pédrot
2016-03-06Removing dependency of Himsg in tactic files.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2016-03-06Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Pierre-Marie Pédrot
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-06Splitting the nsatz ML module into an implementation and a grammar files.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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 14:31:49 +0000