aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-03Merge PR #12953: Add :math: around mathcoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: JasonGross
2020-09-03[bench] Only upload some filesJason Gross
We will now also record a listing of all files that we could have uploaded, in case we want to know what's available to upload in the future.
2020-09-03[bench] Also upload the raw timing files, etcJason Gross
2020-09-03Fix incorrect debruijn handling when Record calls maybe_unify_params_inGaëtan Gilbert
Fix #12887
2020-09-03Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay themPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-03Merge PR #12956: Perform an inversion of control in hint validation for eapply.coqbot-app[bot]
Reviewed-by: mattam82 Ack-by: SkySkimmer Ack-by: ppedrot
2020-09-03Merge PR #12876: Namegen.visible_ids: fixing what seems to be typosPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-03Merge PR #12973: Random cleanup around the data structures used in EqualityHugo Herbelin
Reviewed-by: herbelin
2020-09-03Merge PR #12899: [bench] Update bench script with better urls and more infoPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-03Add Equations overlayMaxime Dénès
2020-09-03Comment AllowedEvars APIMaxime Dénès
2020-09-02Adding change log for #12960.Hugo Herbelin
2020-09-02Fixes #9403 and #10803 (missing flattening of nested applications in notations).Hugo Herbelin
The bugs involved: - a notation with a subterm in position of function of an application - use of this notation in another notation creating a non-flattened application In particular, this fooled "find_appl_head" (for #10803) and the translation from GApp to NApp (for #9403). We fix the translation NApp -> GApp (since glob_constr is supposed to have its applications flattened).
2020-09-02More efficient data structure for allowed evarsMaxime Dénès
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
This is a follow-up of #9062, which introduced a discrenpancy between the two unification engines.
2020-09-02Merge PR #12943: Move Elim-specific codeHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-09-02Remove the opening of CErrors in Elim.Pierre-Marie Pédrot
2020-09-02Code deduplication in Elim.Pierre-Marie Pédrot
2020-09-02Factorize the only uses of internal API in Elim for Inv.Pierre-Marie Pédrot
2020-09-02Make the Elim.branch_args type opaque.Pierre-Marie Pédrot
2020-09-02Further remove the type Elim.branch_assumptions.Pierre-Marie Pédrot
Only one field was used throughout the code base.
2020-09-02Remove unused API from Elim.Pierre-Marie Pédrot
2020-09-02Adding change log for #12946.Hugo Herbelin
2020-09-02Fixes part 1 of #12908 (collision involving a lonely notation).Hugo Herbelin
Strangely, this was not yet noticed. Hiding of a scoped notation by a lonely notation should be checked at printing time.
2020-09-02Document the Equality.equality type in the ML file.Pierre-Marie Pédrot
2020-09-02Remove redundant data from the equality eliminator datatype.Pierre-Marie Pédrot
2020-09-02Do not look for a quantified inductive type in intropattern injection.Pierre-Marie Pédrot
The code below checks that the term is an applied equality, so allowing non-trivially quantified inductive types would trigger an error right after.
2020-09-02Use a dedicated type for equality elimination.Pierre-Marie Pédrot
In this mess of higher-order callbacks it helps sorting out the invariants of the structure.
2020-09-02fix grepping for the Iris commitRalf Jung
2020-09-02CI: build Iris examples instead of lambda-RustRalf Jung
2020-09-02Merge PR #12883: Use a faster algorithm to check for class existence.coqbot-app[bot]
Reviewed-by: mattam82
2020-09-01Merge PR #12872: Unify the shelvesPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: gares Ack-by: mattam82 Reviewed-by: ppedrot
2020-09-01Unify the shelvesMaxime Dénès
Before this patch, the proof engine had three notions of shelves: - A local shelf in `proofview` - A global shelf in `Proof.t` - A future shelf in `evar_map` This has lead to a lot of confusion and limitations or bugs, because some components have only a partial view of the shelf: the pretyper can see only the future shelf, tactics can see only the local and future shelves. In particular, this refactoring is needed for #7825. The solution we choose is to move shelf information to the evar map, as a shelf stack (for nested `unshelve` tacticals). Closes #8770. Closes #6292. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-09-01Merge PR #12892: Update update_global_env usagePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
2020-09-01Merge PR #12961: [declare] Return both declared constants in Derive path.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-01Merge PR #12962: Add zarith to the include path for ocamldebug-coqcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-31Add zarith to the include path for ocamldebug-coqJasper Hugunin
2020-08-31[declare] Return both declared constants in Derive path.Emilio Jesus Gallego Arias
2020-08-31Merge PR #12958: Fix load_printers after zarithcoqbot-app[bot]
Reviewed-by: ejgallego
2020-08-31Update update_global_env usageGaëtan Gilbert
- take just a ugraph instead of the whole env - rename to update_sigma_univs - push global env lookup a bit further up - fix vernacinterp call to update all surrounding proofs, not just the top one - flip argument order for nicer partial applications
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-31Merge PR #12935: Drop opaque bodies of abstracted definitions.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-31Perform an inversion of control in hint validation for eapply.Pierre-Marie Pédrot
We move the "verbose" case to the only point it is actually used. It is a bit unfortunate since it implies a bit of code duplication, but this should not affect runtime since the replaying only happens in case of a user-facing warning.
2020-08-31Fix load_printers after zarithGaëtan Gilbert
2020-08-31Fix mangle names issue in inductionGaëtan Gilbert
Fix #12944
2020-08-31Fixes a freshness issue with induction (see comment in #12944).Hugo Herbelin
The names computed in consume_pattern were lost when calling intros_pattern_core. Moreover, the computation of names to avoid was done several time. We compute it once for all.
2020-08-31Use a faster algorithm to check for class existence.Pierre-Marie Pédrot
There is a hidden invariant that guarantees that the class index and its reference field are the same.
2020-08-31Move elim-specific code from Tacticals to Elim.Pierre-Marie Pédrot
No reason to have them there.
2020-08-30Merge PR #12952: Fix rendering of -> in micromegacoqbot-app[bot]
Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-02 21:34:53 +0000