aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-02
* Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* Avoid warnings about loop indices.Gravatar Guillaume Melquiond2016-01-02
* Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* Proper datatype for EXTEND syntax tokens.Gravatar Pierre-Marie Pédrot2016-01-02
* Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* Fix typos.Gravatar Guillaume Melquiond2016-01-01
* Remove unused hashconsing code.Gravatar Guillaume Melquiond2016-01-01
* Do not make it harder on the compiler optimizer by packing arguments.Gravatar Guillaume Melquiond2016-01-01
* Remove unused functions.Gravatar Guillaume Melquiond2016-01-01
* Remove unplugged button from the interface.Gravatar Guillaume Melquiond2016-01-01
* Remove useless recursive flags.Gravatar Guillaume Melquiond2016-01-01
* Remove unused open.Gravatar Guillaume Melquiond2016-01-01
* Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-01
* Remove unused function Checker.print_loc.Gravatar Guillaume Melquiond2015-12-31
* Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\
* | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
* | Remove Library.mem, which is pointless since 8.5.Gravatar Guillaume Melquiond2015-12-31
| * Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* | Moving apply_type to new proof engine.Gravatar Hugo Herbelin2015-12-30
* | Taking into account generated typing constraints in tactic "generalize".Gravatar Hugo Herbelin2015-12-30
* | 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
| * Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Gravatar Pierre-Marie Pédrot2015-12-29
* | Removing unused parsing entries.Gravatar Pierre-Marie Pédrot2015-12-28
* | Implementing non-focussed generic arguments.Gravatar Pierre-Marie Pédrot2015-12-28
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Gravatar Pierre-Marie Pédrot2015-12-28
* | Factorizing code for untyped constr evaluation.Gravatar Pierre-Marie Pédrot2015-12-27
* | Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
* | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* | Moving basic generalization tactics upwards for possible use in "intros".Gravatar Hugo Herbelin2015-12-25
* | Moving code of specialize so that it can accept "as" (no semantic change).Gravatar Hugo Herbelin2015-12-25
* | Moving specialize to Proofview.tactic.Gravatar Hugo Herbelin2015-12-25
* | Fixing a bug in the order of side conditions for introduction pattern -> and <-.Gravatar Hugo Herbelin2015-12-25
* | Fixing an "injection as" bug in the presence of side conditions.Gravatar Hugo Herbelin2015-12-25
* | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlGravatar Hugo Herbelin2015-12-25
* | Fixing non exhaustive pattern-matching in 003fe3d5e60b.Gravatar Hugo Herbelin2015-12-25
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | Removing the last quoted auto tactic in Tauto.Gravatar Pierre-Marie Pédrot2015-12-24
* | Partial backtrack on commit 20641795624.Gravatar Pierre-Marie Pédrot2015-12-23
* | Avoid a pointless conversion/copy.Gravatar Guillaume Melquiond2015-12-22
* | 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
* | Move the From logic to Loadpath.expand_path.Gravatar Guillaume Melquiond2015-12-22
* | Do not query module files that have already been loaded.Gravatar Guillaume Melquiond2015-12-22
* | ARGUMENT EXTEND shares the toplevel representation when possible.Gravatar Pierre-Marie Pédrot2015-12-21
* | Finer-grained types for toplevel values.Gravatar Pierre-Marie Pédrot2015-12-21
* | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-16 15:29:58 +0000