aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
This feature makes it possible to tell type inference to type applications of a global `foo` using typing information from the context once the `n` first arguments are known. The syntax is: `Arguments foo x y | z`. Closes #7910
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
Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵Enrico Tassi
prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
I don't think there's a reason to treat such variables more severely than unbound variables. This anomaly is often raised by debug printers (e.g. when studying complex scenarios using `Set Unification Debug`), and so makes debugging less convenient. Fixes #3754, fixes #10026.
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
Incidentally, this fixes #10056
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it.
2019-05-09Merge PR #10069: Do not use the constant stack in ↵Hugo Herbelin
whd_betaiota_deltazeta_for_iota_state. Reviewed-by: herbelin
2019-05-07Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.Pierre-Marie Pédrot
There is no point, it is always called with refolding turned off.
2019-05-07[Canonical structures] DeforestationVincent Laporte
2019-04-30Remove the k0 argument from pretype functions.Jasper Hugunin
This was introduced by @herbelin in 817308ab59daa40bef09838cfc3d810863de0e46, appears to have been made unnecessary again by herbelin in 4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6. At this point it appears to be completely unused.
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
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: herbelin Reviewed-by: mattam82 Ack-by: maximedenes
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
Fixes #6699
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
We make clearer which arguments are optional and which are mandatory. Some of these representations are tricky because of small differences between Program and Function, which share the same infrastructure. As a side-effect of this cleanup, Program Fixpoint can now be used with e.g. {measure (m + n) R}. Previously, parentheses were required around R.
2019-04-15Merge PR #9927: Don't store closures in summary (reduction effects)Pierre-Marie Pédrot
Reviewed-by: ppedrot
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
I had to reorganize the code a bit. The Context command moved to comAssumption, as it is not so related to type classes. We were able to remove a few hooks on the way.
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
One other call still remains, but will require to refactor some section-handling code.
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-10Fix constant order in heads.mlMaxime Dénès
As per the OCaml documentation, the order for maps should be total. I also remove some circumvolutions that were added around eliminators and canonical names because of this incorrect order.
2019-04-08Don't store closures in summary (reduction effects)Gaëtan Gilbert
We already have indirection (constant -> effect name, effect name -> function) so we only need to stop using summary.ref for the second map.
2019-04-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
Reviewed-by: gares
2019-04-05[native compiler] Normalize before destructuring sortMaxime Dénès
This was making an assertion fail on https://github.com/coq/coq/issues/9684 after 23f84f37
2019-04-05Remove cache in HeadsMaxime Dénès
This cache makes the pretyper depend on components that should morally be higher-level (Libobject and co), so I'd like to see how critical this cache is before taking any action.
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
Ack-by: jfehrle Ack-by: ppedrot Reviewed-by: vbgl
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-04-02Fast name generation in detyping.Pierre-Marie Pédrot
We provide a flag that allows for a dumber but O(log n) algorithm generating fresh names in detyping.
2019-04-02Abstract away the name generation algorithm in Detyping.Pierre-Marie Pédrot
For now it does not change anything, but it will make the move towards a faster algorithm seamless.
2019-04-02Pass flags through a record in Detyping.Pierre-Marie Pédrot
There was a hidden bug to an unexpected variable capture in decomp_branch. Let us use proper structures to avoid this kind of mess.
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
(warn if bar is a nonprimitive projection)
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-06 21:33:27 +0000