aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-14Reduce the attack surface of Opaqueproof.Pierre-Marie Pédrot
2019-05-14Merge PR #10145: Code cleanups in tacticsHugo Herbelin
2019-05-14Remove the sidecond_first flag of apply-related tactics.Pierre-Marie Pédrot
2019-05-14Remove the elimrename field from Tactics.eliminator.Pierre-Marie Pédrot
2019-05-14Code factorization in elim tactics.Pierre-Marie Pédrot
2019-05-14Overlay for value-returning run_tacticGaëtan Gilbert
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-14Add aucontext debug printerGaëtan Gilbert
2019-05-14Coqc: Ensure that at most one file is given when -o is also given.Hugo Herbelin
2019-05-14Coqc: Ensure exclusiveness of options -quick and -vio2vo.Hugo Herbelin
2019-05-14Usage: Fixing wrong description of load_vernac_object and similar.Hugo Herbelin
2019-05-14Adding missing newline in coqc usage.Hugo Herbelin
2019-05-14CoqIDE: Treat unknown arguments starting with dash as unknown options rather ...Hugo Herbelin
2019-05-14Removing no more existing option -emacs-U.Hugo Herbelin
2019-05-14Usage: fixing indentation for set/unset options.Hugo Herbelin
2019-05-14Ensuring suffix of file to compile also for -vio2vo checking.Hugo Herbelin
2019-05-14Option -check-vio-tasks: fail gracefully when not finding expected integers.Hugo Herbelin
2019-05-14Merge PR #10152: Move last changelog entries for 8.10+beta1.Vincent Laporte
2019-05-13Handle tags shorter than "diff." without an exceptionJim Fehrle
2019-05-13Adding overlay for Equations.Hugo Herbelin
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
2019-05-13Missing change entry for #9854.Théo Zimmermann
2019-05-13Move last changelog entries for 8.10+beta1.Théo Zimmermann
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
2019-05-13Add overlay for UnicoqMaxime Dénès
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
2019-05-13Merge PR #10079: [refman] Move Ltac examples to Ltac chapter.Vincent Laporte
2019-05-12[refman] Raise an error when a notation doesn't parseClément Pit-Claudel
2019-05-12[refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'Clément Pit-Claudel
2019-05-12Merge PR #10083: Avoid trivial (u=u) constraints in AcyclicGraph.constraints_forEmilio Jesus Gallego Arias
2019-05-11Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS ...Pierre-Marie Pédrot
2019-05-11Remove the sidecond_first flag of apply-related tactics.Pierre-Marie Pédrot
2019-05-11Remove the elimrename field from Tactics.eliminator.Pierre-Marie Pédrot
2019-05-11Code factorization in elim tactics.Pierre-Marie Pédrot
2019-05-11Actually use the conversion locality flag.Pierre-Marie Pédrot
2019-05-11Introducing a local flag to hypothesis conversion function.Pierre-Marie Pédrot
2019-05-11Generalize map_named_val to handle whole declarations.Pierre-Marie Pédrot
2019-05-11Abstract the Tactic.e_change_hyps function over the reduction function.Pierre-Marie Pédrot
2019-05-11Merge PR #10052: Cleanup the hypothesis conversion functionHugo Herbelin
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[refman] Mention the `#[canonical(false)]` attributeVincent Laporte
2019-05-10[Attributes] Allow explicit value for two-valued attributesVincent Laporte
2019-05-10Add overlay for elpiVincent Laporte
2019-05-10Changelog for PR #10076Vincent Laporte
2019-05-10[User manual] Fix two warnings related to canonical structuresVincent Laporte
2019-05-10[Canonical structures] “not_canonical” annotation to field declarationsVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 06:49:17 +0000