aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-30Document changes on injection.Maxime Dénès
2014-04-09Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...Pierre Boutillier
2014-04-08Add an option -Q (tentative name).Guillaume Melquiond
2014-04-07Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...Guillaume Melquiond
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2014-01-30Coqmktop without Sys.command, changes in ./configure -*byteflags optionsPierre Letouzey
2014-01-25More in CHANGES.Pierre-Marie Pédrot
2014-01-10Omega: avoiding distinct proof-terms on repeated identical runsPierre Letouzey
2013-12-11Documenting the tactic-in-term construction.Pierre-Marie Pédrot
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-06Document changes and add missing documentation for Program options.msozeau
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
2013-06-02Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anherbelin
2013-05-29Documenting the "appcontext" by default.ppedrot
2013-05-14"change ... in ..." and "simpl ... in ..." now consider nestedherbelin
2013-05-05Reporting the change on matching partial applications in patterns ofherbelin
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
2013-03-21Using hnf instead of "intro H" for forcing reduction to a product.herbelin
2013-03-21Fixing an old pecularity of "red": head betaiota redexes are nowherbelin
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-17Displaying environment and unfolding aliases in "cannot_unify"herbelin
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
2012-08-23CHANGES: document the end of states/initial.coq and coqtop.optletouzey
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-11Some changes in CHANGES.herbelin
2012-08-08Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.herbelin
2012-08-03Document the command Add/Remove Search Blacklistletouzey
2012-08-03re-sync CHANGES with 8.4letouzey
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05Quick update to CHANGES, mention especially the new parsing of ->letouzey
2012-06-05CHANGES: mention the end of induction principles for recordsletouzey
2012-05-29Some documentation of recent changes concerning interfacesletouzey
2012-05-23CHANGES: fix a typo + an entry in the wrong sectionletouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-17Remove the Dp plugin.gmelquio
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-15Update CHANGESherbelin
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
2012-04-12CHANGES: adapt after backport of some features to 8.4letouzey
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-23Documentation of last commit concerning Backtrackingletouzey
2012-03-19More adaptations of pretyping/coercion to Program mode.msozeau
2012-03-19Fix bugs related to Program integration.msozeau
2012-02-07Documentation for Grab Existential Variables.aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 05:35:11 +0000