aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
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-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-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
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-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-24Calling coq references lazily in plugin cc so as to support static linking of...Hugo Herbelin
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-14Fixing OCaml 3.12 compilation.Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-23Fix previous commit on extraction.Maxime Dénès
2015-01-23Extraction: fix #3629.Maxime Dénès
2015-01-12Derive -> derive occurencesPierre Boutillier
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-11Extraction: discard unnecessary code inside modules without signaturesPierre Letouzey
2015-01-11Extraction: no more ascii blob in type variables (fix #3227)Pierre Letouzey
2015-01-11Extraction : some more support functions for a future "Extraction Compute"Pierre Letouzey
2015-01-11Extraction: minor tweaks to ease ongoing experiments about LambdaPierre Letouzey
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:09:39 +0000