| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 2 个月前 | |
Canonicalize the GlobRef map API from Arguments_renaming. | 1 年前 | |
Use variable status to decide if a variable is section variable Termops.is_section_variable is deprecated and a new API Termops.is_section_variable' is added because their types are the same but they need different env arguments so changing in place would be too footgunny. ssr still uses the old "is it in global env" because IDK what it is doing. Fix #18858 | 4 个月前 | |
Program "match" compilation supports inductive types with "let" in indices. | 1 年前 | |
Add missing substitution in cbv for case iv | 3 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 2 个月前 | |
New evar kind for RR variables | 1 年前 | |
[coercions] Disactivate by default the "ambiguous-paths" warning It's a nice but costly-to-check warning. | 23 天前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Generalize get_sigmatypes It assumed a uniform template/poly status for the inductive and its projections, no longer true when e.g. template inductives can have univ or sort polymorphic projections. | 1 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Remove the name field from projections. One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore. | 4 个月前 | |
More type enforced "instantiation" of constr patterns Now we really have `Pattern.constr_pattern` for evaluated patterns, and `[`uninstantiated] Pattern.constr_pattern_r` for globalized but not evaluated patterns. Although it seems to turn the `Any -> user_err ?loc (str "Quotations not allowed in this pattern.")` branch in Patternops.pattern_of_raw into dead code, in fact it was already dead code as the only genarg which has a registered pattern internalization function (for Genintern.generic_intern_pat) is the ltac2 `$` so the only genarg we can see in constr_pattern_r is that one. Then we have 2 cases: - pattern in ltac2 code, in which case it was already using `Uninstantiated` instead of `Any` - other pattern (ltac, Hint Extern, etc), in which case no ltac2 variables are bound so internalization of `$` fails before we reach pattern_of_glob_constr. | 1 年前 | |
Introduce "Univ@{s;l}" notation for sort polymorphism Deprecated old interpretations of Type as Univ (with quickfix) Adapt test-suite to deprecation and update output tests ("breaking" output change) Fix make_anonymous_conclusion_flexible to support `Univ` Add changelog Update documentation of univ-poly Fixup Fix refman Fix typo Stop interpreting Type as Univ. Fix doc, useless if-then-else | 1 个月前 | |
Move Printing Record tables into PrintingFlags | 11 个月前 | |
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 5 个月前 | |
Remove calls to CanOrd in Evaluable. | 1 年前 | |
Remove calls to CanOrd in Evaluable. | 1 年前 | |
Use the now correct set and maps Names APIs. Since the base variants rely on canonical ordering, it makes no sense anymore to have two variants of the same module aliasing the same code. We remove all calls to the _env variants in this commit. | 28 天前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 2 个月前 | |
define_evar_as_sort generate a flexible univ instead of rigid This makes `Check fun A => A -> (A:Set).` succeed. It allows minimization to set in `Inductive T A := C : A -> T (option A) -> T A.` to produce `T : Set -> Set` which is a bit aggressive. Considering `Inductive T A := C : T (option A) -> T A.` already minimized the type of A to Set this is probably not worth avoiding. | 13 天前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Use the now correct set and maps Names APIs. Since the base variants rely on canonical ordering, it makes no sense anymore to have two variants of the same module aliasing the same code. We remove all calls to the _env variants in this commit. | 28 天前 | |
Undo adhoc exclusion of RR evar unification | 5 个月前 | |
Add support for parsing elimination constraints | 10 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Added APIs for coqlsp | 6 个月前 | |
Added APIs for coqlsp | 6 个月前 | |
More precise typing in genarg register default value | 1 年前 | |
Stop using genarg for constr syntax extension Instead we have a separate Dyn | 8 个月前 | |
Enforce that genarg interp functions are at the correct type It never made any sense to be able to declare an interp function with top type = Empty.t. We add a new Val.tag "Any" for genargs whose top type is Val.t without a dedicated dyn tag (typically ltac2 in 1 quotation genargs). | 8 个月前 | |
Enforce that genarg interp functions are at the correct type It never made any sense to be able to declare an interp function with top type = Empty.t. We add a new Val.tag "Any" for genargs whose top type is Val.t without a dedicated dyn tag (typically ltac2 in 1 quotation genargs). | 8 个月前 | |
Stop using genarg for constr syntax extension Instead we have a separate Dyn | 8 个月前 | |
Stop using genarg for constr syntax extension Instead we have a separate Dyn | 8 个月前 | |
Remove the name field from projections. One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore. | 4 个月前 | |
Use variable status to decide if a variable is section variable Termops.is_section_variable is deprecated and a new API Termops.is_section_variable' is added because their types are the same but they need different env arguments so changing in place would be too footgunny. ssr still uses the old "is it in global env" because IDK what it is doing. Fix #18858 | 4 个月前 | |
Introduce "Univ@{s;l}" notation for sort polymorphism Deprecated old interpretations of Type as Univ (with quickfix) Adapt test-suite to deprecation and update output tests ("breaking" output change) Fix make_anonymous_conclusion_flexible to support `Univ` Add changelog Update documentation of univ-poly Fixup Fix refman Fix typo Stop interpreting Type as Univ. Fix doc, useless if-then-else | 1 个月前 | |
Introduce "Univ@{s;l}" notation for sort polymorphism Deprecated old interpretations of Type as Univ (with quickfix) Adapt test-suite to deprecation and update output tests ("breaking" output change) Fix make_anonymous_conclusion_flexible to support `Univ` Add changelog Update documentation of univ-poly Fixup Fix refman Fix typo Stop interpreting Type as Univ. Fix doc, useless if-then-else | 1 个月前 | |
QGlobal is not QVar | 7 个月前 | |
Keep track of variable status (secvar or not) in named contexts Close #6773 | 4 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
fix: catch QGraph.EliminationError in make_allowed_elimination_actions | 12 天前 | |
Store template inductive data abstracted w.r.t. template levels. All accesses to terms and sorts from a template inductive block need first to substitute the bound levels by the default template instance, just like polymorphic inductive types. Thanks to the invariants on template types, there is actually little additional work to do, because template levels can only appear in the type of parameters (not in lets!) or in the conclusion. | 4 个月前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 2 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
case styles MatchStyle and RegularStyle are the same | 8 个月前 | |
Add Scheme All Command | 9 个月前 | |
document tactics/tactics.mli | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Enable warning 70 (missing mli), add mli files I am tired of seeing compilation bottleneck on random grammar files | 3 年前 | |
fix readback lifting bug | 21 天前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Stop using genarg for constr syntax extension Instead we have a separate Dyn | 8 个月前 | |
Stop using genarg for constr syntax extension Instead we have a separate Dyn | 8 个月前 | |
Stop using genarg for constr syntax extension Instead we have a separate Dyn | 8 个月前 | |
clean up exceptions of recursion_scheme_error | 10 个月前 | |
clean up exceptions of recursion_scheme_error | 10 个月前 | |
Fix Template application with 3 arguments needlessly unifying qvars to Prop Fix #22592 | 12 天前 | |
Collapse sort variables to Prop if they are >= Prop but not <= Type Fix #22152 The "above prop" data in ustate now contains whether we only need `Prop <= q` or if `q <= Type` may be needed. Currently enforcing a constraint `q <= Type` actually forces `q == Type`, so `q <= Type` come from 2 cases: - template poly - when interpreting explicit `Type` in a potentially-template inductive (otherwise something like `Inductive I (P:Type -> ...) := C (_: P True)` produces `P:Prop -> ...`) | 4 个月前 | |
Use the now correct set and maps Names APIs. Since the base variants rely on canonical ordering, it makes no sense anymore to have two variants of the same module aliasing the same code. We remove all calls to the _env variants in this commit. | 28 天前 | |
Use the now correct set and maps Names APIs. Since the base variants rely on canonical ordering, it makes no sense anymore to have two variants of the same module aliasing the same code. We remove all calls to the _env variants in this commit. | 28 天前 | |
Fix blatant bug in Program's papp | 1 个月前 | |
Rename Coq -> Rocq in various comments and doc Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> Co-authored-by: Guillaume Melquiond <guillaume.melquiond@inria.fr> | 1 年前 | |
Use the now correct set and maps Names APIs. Since the base variants rely on canonical ordering, it makes no sense anymore to have two variants of the same module aliasing the same code. We remove all calls to the _env variants in this commit. | 28 天前 | |
Merge PR #22077: Reduction effects use econstr Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 4 个月前 | |
Remove the name field from projections. One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore. | 4 个月前 | |
Reduce the exposure of QualityOrSet.t type in the Retyping API. This horrendous type should never have escaped from its very specific use-case, namely to be able to have separate induction principles for predicates returning a Set or a Type. We expose a proper retyping primitive giving direct access to the quality, which is what most users actually rely on. | 5 个月前 | |
Use the now correct set and maps Names APIs. Since the base variants rely on canonical ordering, it makes no sense anymore to have two variants of the same module aliasing the same code. We remove all calls to the _env variants in this commit. | 28 天前 | |
Move Printing Record tables into PrintingFlags | 11 个月前 | |
More informative error message for "not an inductive product" Fix #7996 | 3 个月前 | |
More informative error message for "not an inductive product" Fix #7996 | 3 个月前 | |
Kernel keep qvar information for template inductives | 1 年前 | |
Kernel keep qvar information for template inductives | 1 年前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 2 个月前 | |
Canonicalize the GlobRef map API from Typeclasses. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 2 年前 | |
Merge PR #22087: Move check_hyps_inclusion out of the kernel Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 4 个月前 | |
feat: Add elaboration of fresh qualities Currently behind a Sort Polymorphism flag. fix: Generate proper sort variable in record feat: Add sort elab for interactive definitions fix: Thread sort poly flag more correctly It was being passed as unconstrained_sorts in some cases. refactor: Remove unnecessary sort_poly flags fix: Add sort_poly to prepare_obligations refactor: Remove remaining fixmes and todos refactor: General cleanup refactor: Get ?evar_handler from evd refactor: Remove search_fix_guard doc: comment collapse refactor: Remove unnecessary unconstrained_sorts refactor: Remove unnecessary check for collapse_sort_variables revert: Some changes in unify quality feat: Add elim constraints to non-prim records with sort variables doc: Add doc on flag + implicit elab of sorts chore: Add changelog entry chore: Add overlays refactor: indentation feat: Add more specific elim constraints to non-prim projections Address comments refactor: Pass on sigma in search_guard test: Move sort_poly_elab test to output folder fix: Change assert implicit sort vars for error in sections fix(attempt): Return evd from make_recursive_bodies refactor: Change option array to list option refactor: Use Cmap_env to keep elim constraints from projs Apply suggestion from @SkySkimmer update test | 8 个月前 | |
unification: protect CS resolution against call on illtyped terms | 4 个月前 | |
`rewrite in` no subterm error mention hyp instead of saying "in goal" | 8 个月前 | |
Merge PR #22574: fix readback lifting bug Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 14 天前 | |
Allow normalizing constructor parameters in the VM. For backwards compatibility and efficiency, we parameterize this behaviour by a flag that is not user-available. Note also that we normalize the parameters through the kernel rather than through the VM, as there is a smaller compilation time overhead and parameters should not be computation-intensive. | 4 个月前 |
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
| 2 个月前 | ||
| 1 年前 | ||
| 4 个月前 | ||
| 1 年前 | ||
| 3 个月前 | ||
| 2 年前 | ||
| 2 个月前 | ||
| 1 年前 | ||
| 23 天前 | ||
| 2 年前 | ||
| 1 个月前 | ||
| 2 年前 | ||
| 4 个月前 | ||
| 1 年前 | ||
| 1 个月前 | ||
| 11 个月前 | ||
| 5 个月前 | ||
| 1 年前 | ||
| 1 年前 | ||
| 28 天前 | ||
| 2 个月前 | ||
| 13 天前 | ||
| 2 年前 | ||
| 28 天前 | ||
| 5 个月前 | ||
| 10 个月前 | ||
| 2 年前 | ||
| 6 个月前 | ||
| 6 个月前 | ||
| 1 年前 | ||
| 8 个月前 | ||
| 8 个月前 | ||
| 8 个月前 | ||
| 8 个月前 | ||
| 8 个月前 | ||
| 4 个月前 | ||
| 4 个月前 | ||
| 1 个月前 | ||
| 1 个月前 | ||
| 7 个月前 | ||
| 4 个月前 | ||
| 2 年前 | ||
| 12 天前 | ||
| 4 个月前 | ||
| 2 个月前 | ||
| 2 年前 | ||
| 8 个月前 | ||
| 9 个月前 | ||
| 1 年前 | ||
| 2 年前 | ||
| 2 年前 | ||
| 3 年前 | ||
| 21 天前 | ||
| 2 年前 | ||
| 8 个月前 | ||
| 8 个月前 | ||
| 8 个月前 | ||
| 10 个月前 | ||
| 10 个月前 | ||
| 12 天前 | ||
| 4 个月前 | ||
| 28 天前 | ||
| 28 天前 | ||
| 1 个月前 | ||
| 1 年前 | ||
| 28 天前 | ||
| 4 个月前 | ||
| 4 个月前 | ||
| 5 个月前 | ||
| 28 天前 | ||
| 11 个月前 | ||
| 3 个月前 | ||
| 3 个月前 | ||
| 1 年前 | ||
| 1 年前 | ||
| 2 个月前 | ||
| 1 年前 | ||
| 2 年前 | ||
| 2 年前 | ||
| 4 个月前 | ||
| 8 个月前 | ||
| 4 个月前 | ||
| 8 个月前 | ||
| 14 天前 | ||
| 4 个月前 |