aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
2017-10-24Typo in comment in tactic_matching.ml.Hugo Herbelin
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
2017-10-09Merge PR #1087: [stm] Switch to a functional APIMaxime Dénès
2017-10-09Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...Maxime Dénès
2017-10-09Merge PR #1114: Generic handling of nameable objects for pluginsMaxime Dénès
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-10-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
2017-10-04Merge PR #1078: Report missing arguments in error messageMaxime Dénès
2017-10-03Ltac uses the new generic locatable API.Pierre-Marie Pédrot
2017-10-03Moving the Ltac-specific part of the nametab to the Ltac plugin.Pierre-Marie Pédrot
2017-10-03Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Maxime Dénès
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-26Properly display the "only" prefix for selectors (bug #5760).Guillaume Melquiond
2017-09-21Report missing arguments in error messageTej Chajed
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-31Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameMaxime Dénès
2017-08-29Merge PR #946: Functional pretyping interfaceMaxime Dénès
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-08-29Adapting code to renaming Option.fold_map -> Option.fold_left_map.Hugo Herbelin
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
2017-08-16Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsMaxime Dénès
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
2017-08-01Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.Maxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Removing default evar-normalization for ARGUMENT EXTEND.Pierre-Marie Pédrot
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-19Merge PR #770: [proof] Move bullets to their own module.Maxime Dénès
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-27Preparing to hints supporting discharge.Hugo Herbelin
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#763: [proof] Deprecate redundant wrappers.Maxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
2017-06-14Deprecate options that were introduced for compatibility with 8.2.Guillaume Melquiond
2017-06-14Remove support for Coq 8.2.Guillaume Melquiond
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-12[proof] Move bullets to their own module.Emilio Jesus Gallego Arias
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Remove (useless) aliases from the API.Matej Košík
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 08:23:04 +0000