aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-04-15Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type.Hugo Herbelin
2016-04-14This is an attempt to clarify terminology in choosing variable namesHugo Herbelin
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-13Uniformizing the semantics of ARGUMENT EXTEND macros.Pierre-Marie Pédrot
2016-04-12Adding toplevel representation sharing for some generic arguments.Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-04-12Adding warnings for inferrable *_TYPED AS clauses.Pierre-Marie Pédrot
2016-04-12Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.Pierre-Marie Pédrot
2016-04-12Warning for redundant TYPED AS clauses.Pierre-Marie Pédrot
2016-04-12Allowing simple ARGUMENT EXTEND not to mention their self type.Pierre-Marie Pédrot
2016-04-12Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.Pierre-Marie Pédrot
2016-04-12Fixing printing of "destruct in" after ce71ac17268f.Hugo Herbelin
2016-04-11Removing the typed-level tactic_expr type.Pierre-Marie Pédrot
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-10Extruding the print_atom primitive.Pierre-Marie Pédrot
2016-04-10Expliciting the fact that the atomic tactic type is self-contained.Pierre-Marie Pédrot
2016-04-09A small test of Print Ltac.Hugo Herbelin
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Removing automatic printing of leading space in auto_using andHugo Herbelin
2016-04-09Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...Hugo Herbelin
2016-04-09Simplifying code for printing VERNAC EXTEND.Hugo Herbelin
2016-04-09Fixing extra space in printing inductive types with no explicit type given.Hugo Herbelin
2016-04-09In pr_clauses, do not print a leading space by default so that it canHugo Herbelin
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Added compatibility coercions from Specif.v which were present in Coq 8.4.Hugo Herbelin
2016-04-08Fixing a source of inefficiency and an artificial dependency in theDaniel de Rauglaudre
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-04-08Fixing printing of Tactic Notations with tactic arguments.Pierre-Marie Pédrot
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
2016-04-07Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-04-07Merge PR#152: Add -compat 8.4 econstructor tactics, and testsMaxime Dénès
2016-04-07An example which failed in 8.5 and that d670c6b6 fixes.Hugo Herbelin
2016-04-07Use -win32 and -win64 suffixes for installer name on Windows.Maxime Dénès
2016-04-05Add -compat 8.4 econstructor tactics, and testsJason Gross
2016-04-05Fix bug #4656Jason Gross
2016-04-04Update Coq84.vJason Gross
2016-04-04Add compatibility Nonrecursive Elimination SchemesJason Gross
2016-04-04Fix after merge, the revert of Bind Scope applies to trunk only.Matthieu Sozeau
2016-04-04Merge remote-tracking branch 'origin/pr/78' into trunk:Maxime Dénès
2016-04-04Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkMatej Kosik
2016-04-04Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...Matej Kosik
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-04-04Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Matthieu Sozeau
2016-04-03Fixing the "No applicable tactic" non informative error messageHugo Herbelin
2016-04-01Getting rid of the "_mods" parsing entry.Pierre-Marie Pédrot
2016-03-31Providing an API to access the parsing engine summary in a first-class way.Pierre-Marie Pédrot
2016-03-31Adding a test for bug #1850.Pierre-Marie Pédrot
2016-03-31Moving the code handling tactic notations to Tacentries.Pierre-Marie Pédrot
2016-03-31Abstracting away the Summary-synchronized grammar-modifying commands.Pierre-Marie Pédrot
2016-03-31Moving the Tactic Notation entry parser from Pcoq to Tacentries.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-24 15:22:54 +0000