aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2019-04-10Remove calls to Global.env from EvarsolveMaxime Dénès
2019-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-10Remove calls to Global.env in TypingMaxime Dénès
2019-04-10Remove calls to Global.env in Glob_opsMaxime Dénès
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Remove call to global env in pretyping.mlMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-10Fix constant order in heads.mlMaxime Dénès
2019-04-08Don't store closures in summary (reduction effects)Gaëtan Gilbert
2019-04-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
2019-04-05[native compiler] Normalize before destructuring sortMaxime Dénès
2019-04-05Remove cache in HeadsMaxime Dénès
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02Fast name generation in detyping.Pierre-Marie Pédrot
2019-04-02Abstract away the name generation algorithm in Detyping.Pierre-Marie Pédrot
2019-04-02Pass flags through a record in Detyping.Pierre-Marie Pédrot
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-30[Canonical structures] Minor refactoringVincent Laporte
2019-03-30[Canonical structures] Minor cleaningVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:08:10 +0000