aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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
2015-12-18TYPOGRAPHY: correction of one particular error in the Reference ManualMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Matej Kosik
2015-12-18CLEANUP: simplifying "Coqtop.init_gc" implementationMatej Kosik
2015-12-18CLEANUP: removing unnecessary wrapper functionMatej Kosik
2015-12-18COMMENTS: added to some variants of "Globalnames.global_reference" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of "Glob_term.glob_constr" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of the "Constrexpr.prim_token" type.Matej Kosik
2015-12-18ALPHA-CONVERSION: in "parsing/g_vernac.ml4" fileMatej Kosik
2015-12-18COMMENTS: added to the "Unicode" module.Matej Kosik
2015-12-18COMMENTS: updated in the "Option" module.Matej Kosik
2015-12-18COMMENTS: added to some variants of the "Constr.kind_of_term" type.Matej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-12-18COMMENTS: added to the "Predicate" moduleMatej Kosik
2015-12-18COMMENTS: added to the "Names" module.Matej Kosik
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convMatej Kosik
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reductionops moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-16Updating credits.Hugo Herbelin
2015-12-16Update version numbers and magic numbers for 8.5rc1 release.Maxime Dénès
2015-12-16FIx parsing of tactic "simple refine".Maxime Dénès
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-16Extraction: slightly better heuristic for Obj.magic simplificationsPierre Letouzey
2015-12-16Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsPierre Letouzey
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Fix test suite after change in extraction.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 05:02:25 +0000