aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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-15Merge branch 'v8.5'Pierre-Marie Pédrot
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-09Merge branch 'v8.5' into trunkPierre Letouzey
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-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-25Correcting a bug introduced by universes polymorphismjforest
2015-03-25correcting a bug with aliased when using Functional Schemeforest
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-21Avoid segfault from code extracted to ghc. (Fix for bug #1257)Guillaume Melquiond
2015-03-21Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Guillaume Melquiond
2015-03-21Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Guillaume Melquiond
2015-03-13Merge branch 'v8.5' into trunkArnaud Spiwack
2015-03-13Declarative mode: make it so that unfocussing can only be done for closed sub...Arnaud Spiwack
2015-03-13Declarative mode: remove dead code.Arnaud Spiwack
2015-03-13Declarative mode: remove a superfluous [set_proof_mode].Arnaud Spiwack
2015-03-13Declarative mode: fix the focus behaviour.Arnaud Spiwack
2015-03-13rewiring Czar printers that were disabledPierre Corbineau
2015-03-11Fix double print in decl_mode.Enrico Tassi
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-03Fix bug #3732: firstorder was using detyping to build existentialMatthieu Sozeau
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
2015-03-02rewiring Czar printers that were disabledPierre Corbineau
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-24Calling coq references lazily in plugin cc so as to support static linking of...Hugo Herbelin
2015-02-23Merge branch 'v8.5' into trunkEnrico Tassi
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-23Partially porting eauto to the new tactic API.Pierre-Marie Pédrot
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 16:00:44 +0000