aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Improve directives for Haskell extraction of nat.Gravatar Maxime Dénès2015-09-03
* Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.vGravatar Nickolai Zeldovich2015-09-03
* Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.vGravatar Nickolai Zeldovich2015-09-03
* Extraction: fix primitive projection extraction.Gravatar Matthieu Sozeau2015-07-22
* Add efficient extraction of [nat], [Z], and [string] to HaskellGravatar Nickolai Zeldovich2015-06-22
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Rationalizing a bit the interface of Hints.Gravatar Pierre-Marie Pédrot2015-05-11
* Fix bug #4212, congruence forgetting about some universe constraints.Gravatar Matthieu Sozeau2015-05-05
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Declarative mode: remaining goals are "given up" when closing blocks.Gravatar Arnaud Spiwack2015-04-22
* Remove dirty debug printing from funind.Gravatar Maxime Dénès2015-04-15
* Function now supports puniveresGravatar jforest2015-04-14
* better debug in recdefGravatar jforest2015-04-14
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
* correction of a bug reported by Tristan CrolardGravatar jforest2015-04-13
* Fixing bug #4186.Gravatar Pierre-Marie Pédrot2015-04-13
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* JSON extraction: make explicit each group of mutually-recursive fixpointsGravatar Nickolai Zeldovich2015-04-09
* JSON extraction: construct full names (dot-separated) in pp_globalGravatar Nickolai Zeldovich2015-04-09
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
* add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.vGravatar Nickolai Zeldovich2015-04-08
* Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)Gravatar Nickolai Zeldovich2015-04-08
* Puts all the "import" statements first so as to accommodate the latest GHC.Gravatar Nickolai Zeldovich2015-04-02
* Fix some typos.Gravatar Guillaume Melquiond2015-04-02
* Define Any in Haskell extraction when Tunknown is used.Gravatar Nickolai Zeldovich2015-04-02
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
* Declarative mode: fix proof modes.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: fix vernac classification.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: plug the specialised printers back.Gravatar Arnaud Spiwack2015-03-31
* Correcting a bug introduced by universes polymorphismGravatar jforest2015-03-25
* correcting a bug with aliased when using Functional SchemeGravatar forest2015-03-25
* Avoid segfault from code extracted to ghc. (Fix for bug #1257)Gravatar Guillaume Melquiond2015-03-21
* Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Gravatar Guillaume Melquiond2015-03-21
* Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Gravatar Guillaume Melquiond2015-03-21
* Declarative mode: make it so that unfocussing can only be done for closed sub...Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: remove dead code.Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: remove a superfluous [set_proof_mode].Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: fix the focus behaviour.Gravatar Arnaud Spiwack2015-03-13
* rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-13
* Fix double print in decl_mode.Gravatar Enrico Tassi2015-03-11
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Fix bug #3732: firstorder was using detyping to build existentialGravatar Matthieu Sozeau2015-03-03
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* Calling coq references lazily in plugin cc so as to support static linking of...Gravatar Hugo Herbelin2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-14
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:02:32 +0000