aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-18Fix a bug preventing the generation of graphs when doing multipleMatthieu Sozeau
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-28Do not pause globing in funind. (Fix bug #4382)Guillaume Melquiond
2015-10-19Partly fixes #3225. Removed some old experimental stuff in funind.Pierre Courtieu
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-08f_equal fix continued: do a refresh_universes as before.Matthieu Sozeau
2015-10-07Fix bug #4069: f_equal regression.Matthieu Sozeau
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs: fix evar_map initialization in newring.Matthieu Sozeau
2015-10-02Univs: fix evar_map leaks bugs in FunctionMatthieu Sozeau
2015-10-02Univs: fix an evar leak in congruenceMatthieu Sozeau
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-09-03Improve directives for Haskell extraction of nat.Maxime Dénès
2015-09-03Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.vNickolai Zeldovich
2015-09-03Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.vNickolai Zeldovich
2015-07-22Extraction: fix primitive projection extraction.Matthieu Sozeau
2015-06-22Add efficient extraction of [nat], [Z], and [string] to HaskellNickolai Zeldovich
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-11Rationalizing a bit the interface of Hints.Pierre-Marie Pédrot
2015-05-05Fix bug #4212, congruence forgetting about some universe constraints.Matthieu Sozeau
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-23Using tclZEROMSG instead of tclZERO in several places.Pierre-Marie Pédrot
2015-04-22Declarative mode: remaining goals are "given up" when closing blocks.Arnaud Spiwack
2015-04-15Remove dirty debug printing from funind.Maxime Dénès
2015-04-14Function now supports puniveresjforest
2015-04-14better debug in recdefjforest
2015-04-14Opaque implementation of auto tactics.Pierre-Marie Pédrot
2015-04-13correction of a bug reported by Tristan Crolardjforest
2015-04-13Fixing bug #4186.Pierre-Marie Pédrot
2015-04-10Fix #3590 for good this time, by changing the API, change's argument nowMatthieu Sozeau
2015-04-09JSON extraction: make explicit each group of mutually-recursive fixpointsNickolai Zeldovich
2015-04-09JSON extraction: construct full names (dot-separated) in pp_globalNickolai Zeldovich
2015-04-09Add extraction to JSON.Nickolai Zeldovich
2015-04-08add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.vNickolai Zeldovich
2015-04-08Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)Nickolai Zeldovich
2015-04-02Puts all the "import" statements first so as to accommodate the latest GHC.Nickolai Zeldovich
2015-04-02Fix some typos.Guillaume Melquiond
2015-04-02Define Any in Haskell extraction when Tunknown is used.Nickolai Zeldovich
2015-04-01Accomodating #4166 (providing "Require Import OmegaTactic" as aHugo Herbelin
2015-03-31Declarative mode: fix proof modes.Arnaud Spiwack
2015-03-31Declarative mode: fix vernac classification.Arnaud Spiwack
2015-03-31Declarative mode: plug the specialised printers back.Arnaud Spiwack
2015-03-25Correcting a bug introduced by universes polymorphismjforest
2015-03-25correcting a bug with aliased when using Functional Schemeforest
2015-03-21Avoid segfault from code extracted to ghc. (Fix for bug #1257)Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:12:51 +0000