aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-01-28Merge PR #11379: [ocaml] Remove Custom Backtrace module in favor of OCaml'sPierre-Marie Pédrot
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-21Typo in an anomaly message.Hugo Herbelin
2020-01-16[mltop] Remove error handling hacks in favor of default methods.Emilio Jesus Gallego Arias
2020-01-16[mltop] Store digest of modules used to compile files.Emilio Jesus Gallego Arias
2020-01-15[ocaml] Remove Custom Backtrace module in favor of OCaml'sEmilio Jesus Gallego Arias
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-09Fix build after merge of #11164Gaëtan Gilbert
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Add Set NativeCompute TimingJason Gross
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-29Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a unificatio...Pierre-Marie Pédrot
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-27Merge PR #11315: Ensure that a custom entry cannot be defined twice.Hugo Herbelin
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-23Merge PR #11293: Rename files with Class in their name to make their role cle...Hugo Herbelin
2019-12-23Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.Hugo Herbelin
2019-12-23Merge PR #11274: [library] [cleanup] Remove code duplication.Pierre-Marie Pédrot
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-22Centralize the flag handling native compilation.Pierre-Marie Pédrot
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-16Don't pass (ignored) implicits to interp_mutual_inductive_constrGaëtan Gilbert
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-12-16reduce arguments of template_polymorphism_candidateGaëtan Gilbert
2019-12-16comInductive: remove redundant check_evars callsGaëtan Gilbert
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
2019-12-10[library] [cleanup] Remove code duplication.Emilio Jesus Gallego Arias
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-12-08When printing term together with its type, use info that term is in context.Hugo Herbelin
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-04Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.Hugo Herbelin
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-27Remove deprecated commands `AddPath`, `AddRecPath` and `DelPath`Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 16:27:03 +0000