aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Bug fix : variable capture in ltac code of NsatzGravatar thery2016-07-05
* congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
* congruence: remove casts of indexed termsGravatar Matthieu Sozeau2016-07-04
* congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
* Fix typo.Gravatar Guillaume Melquiond2016-06-23
* Merge branch 'bug4725' into v8.5Gravatar Matthieu Sozeau2016-06-14
|\
* | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| * Univs/Program/Function: Fix bug #4725Gravatar Matthieu Sozeau2016-05-26
|/
* Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
* Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
* Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
* Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
* Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vGravatar Nickolai Zeldovich2016-04-09
* Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 23:34:23 +0000