aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Fix typos.Gravatar Guillaume Melquiond2016-01-01
* Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\
* | Simplifying code of fourier.Gravatar Hugo Herbelin2015-12-30
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Gravatar Pierre-Marie Pédrot2015-12-28
* | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
| * Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* | Changing the toplevel type of the int_or_var generic type to int.Gravatar Pierre-Marie Pédrot2015-12-21
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | Removing redundant versions of generalize.Gravatar Hugo Herbelin2015-12-05
* | Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
* | Getting rid of dynamic hacks in Setoid_newring.Gravatar Pierre-Marie Pédrot2015-12-04
* | Removing the last use of tacticIn in setoid_ring.Gravatar Pierre-Marie Pédrot2015-12-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
| * 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
* | Preventing an unwanted warning 5 "this function application is partial"Gravatar Hugo Herbelin2015-11-07
* | Merge remote-tracking branch 'origin/v8.5' into upstream-trunkGravatar Hugo Herbelin2015-11-07
|\|
| * Fixing complexity issue with f_equal. Thanks to J.-H. JourdanGravatar Hugo Herbelin2015-11-06
* | Monotonizing Tactics.change_arg.Gravatar Pierre-Marie Pédrot2015-10-29
* | Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * 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
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 18:08:18 +0000