aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-22Merge PR #9062: Delay the computation of frozen evars in legacy unification.Matthieu Sozeau
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-24Merge PR #10536: Fix #10533: uncaught Invalid_argument Array.fold_left2 in re...Enrico Tassi
2019-07-22[Pretyping] Do not use the stale evarmap (in thin_evars)Vincent Laporte
2019-07-19Fix #10533: uncaught Invalid_argument Array.fold_left2 in rewriteGaëtan Gilbert
2019-07-16Move unfold_side_flags CClosure -> Tacred internalsGaëtan Gilbert
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-07-03Merge PR #10419: [api] Refactor most of `Decl_kinds`Gaëtan Gilbert
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
2019-07-01[pretyping] Remove seemingly unless check about "variable" opacity.Emilio Jesus Gallego Arias
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-06-03Expose set interface to option tablesGaëtan Gilbert
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-05-19Make the type of constant bodies parametric on opaque proofs.Pierre-Marie Pédrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
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-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-05-10[Canonical structures] “not_canonical” annotation to field declarationsVincent Laporte
2019-05-10[Canonical structures] Some projections may not be canonicalVincent Laporte
2019-05-10Remove various circumvolutions from reduction behaviorsMaxime Dénès
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-09Merge PR #10069: Do not use the constant stack in whd_betaiota_deltazeta_for_...Hugo Herbelin
2019-05-07Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.Pierre-Marie Pédrot
2019-05-07[Canonical structures] DeforestationVincent Laporte
2019-04-30Remove the k0 argument from pretype functions.Jasper Hugunin
2019-04-29Fix variant of #9344 for native_computeMaxime Dénès
2019-04-29Fix #9344, #9348: incorrect unsafe to_constr in vnormGaëtan Gilbert
2019-04-25inferCumulativity: shortcut for all-Invariant inductivesGaëtan Gilbert
2019-04-16Merge PR #9165: Recarg cleanupEmilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-04-15Merge PR #9927: Don't store closures in summary (reduction effects)Pierre-Marie Pédrot
2019-04-10Remove calls to Global.env in HeadsMaxime Dénès
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:57:45 +0000