aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-01-01Remove unused functions.Guillaume Melquiond
2016-01-01Remove unplugged button from the interface.Guillaume Melquiond
2016-01-01Remove useless recursive flags.Guillaume Melquiond
2016-01-01Remove unused open.Guillaume Melquiond
2016-01-01Remove duplicate declarations.Guillaume Melquiond
2015-12-31Remove unused function Checker.print_loc.Guillaume Melquiond
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-31Remove Library.mem, which is pointless since 8.5.Guillaume Melquiond
2015-12-31Do not dump a glob reference when its location is ghost. (Fix bug #4469)Guillaume Melquiond
2015-12-30Moving apply_type to new proof engine.Hugo Herbelin
2015-12-30Taking into account generated typing constraints in tactic "generalize".Hugo Herbelin
2015-12-30Simplifying code of fourier.Hugo Herbelin
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-29Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Pierre-Marie Pédrot
2015-12-28Removing unused parsing entries.Pierre-Marie Pédrot
2015-12-28Implementing non-focussed generic arguments.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-28Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Pierre-Marie Pédrot
2015-12-27Factorizing code for untyped constr evaluation.Pierre-Marie Pédrot
2015-12-27Removing dead code.Pierre-Marie Pédrot
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-12-25Moving basic generalization tactics upwards for possible use in "intros".Hugo Herbelin
2015-12-25Moving code of specialize so that it can accept "as" (no semantic change).Hugo Herbelin
2015-12-25Moving specialize to Proofview.tactic.Hugo Herbelin
2015-12-25Fixing a bug in the order of side conditions for introduction pattern -> and <-.Hugo Herbelin
2015-12-25Fixing an "injection as" bug in the presence of side conditions.Hugo Herbelin
2015-12-25Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlHugo Herbelin
2015-12-25Fixing non exhaustive pattern-matching in 003fe3d5e60b.Hugo Herbelin
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-24Removing the last quoted auto tactic in Tauto.Pierre-Marie Pédrot
2015-12-23Partial backtrack on commit 20641795624.Pierre-Marie Pédrot
2015-12-22Avoid a pointless conversion/copy.Guillaume Melquiond
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-22Move the From logic to Loadpath.expand_path.Guillaume Melquiond
2015-12-22Do not query module files that have already been loaded.Guillaume Melquiond
2015-12-21ARGUMENT EXTEND shares the toplevel representation when possible.Pierre-Marie Pédrot
2015-12-21Finer-grained types for toplevel values.Pierre-Marie Pédrot
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Sharing toplevel representation for several generic types.Pierre-Marie Pédrot
2015-12-21Changing the toplevel type of the int_or_var generic type to int.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-21Attaching a dynamic argument to the toplevel type of generic arguments.Pierre-Marie Pédrot
2015-12-21Trust the directory cache in batch mode.Guillaume Melquiond
2015-12-18COMMENTS: added to the "Constr.case_info" type.Matej Kosik
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-18CLEANUP: removing unnecessary aliasMatej Kosik
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 08:21:04 +0000