aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* Extraction: slightly better heuristic for Obj.magic simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: more cautious use of intermediate result caching (fix #3923)Gravatar Pierre Letouzey2015-12-15
* Extraction: fix a few little glitches with my last commit (replacing unused v...Gravatar Pierre Letouzey2015-12-15
* Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Gravatar Pierre Letouzey2015-12-14
* Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Gravatar Pierre Letouzey2015-12-14
* Extraction: cosmetically avoid generating spaces on empty linesGravatar Pierre Letouzey2015-12-14
* Extraction: also get rid of explicit '\n' for haskellGravatar Pierre Letouzey2015-12-14
* Extraction: fix a pretty-print issueGravatar Pierre Letouzey2015-12-14
* Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Gravatar Pierre Letouzey2015-12-14
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Extraction: check for remaining implicits after dead code removal (fix #4243)Gravatar Pierre Letouzey2015-12-12
* Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Gravatar Pierre Letouzey2015-12-12
* Extraction: avoid generating some blanks at end-of-lineGravatar Pierre Letouzey2015-12-12
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Fix a bug preventing the generation of graphs when doing multipleGravatar Matthieu Sozeau2015-11-18
* Fixing complexity issue with f_equal. Thanks to J.-H. JourdanGravatar Hugo Herbelin2015-11-06
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
* Do not pause globing in funind. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-28
* Partly fixes #3225. Removed some old experimental stuff in funind.Gravatar Pierre Courtieu2015-10-19
* Exporting the original unprocessed hint in the hint running function.Gravatar Pierre-Marie Pédrot2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* f_equal fix continued: do a refresh_universes as before.Gravatar Matthieu Sozeau2015-10-08
* Fix bug #4069: f_equal regression.Gravatar Matthieu Sozeau2015-10-07
* Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map initialization in newring.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
* Univs: fix an evar leak in congruenceGravatar Matthieu Sozeau2015-10-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 03:19:45 +0000