aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-08-30Add :math: around mathJason Gross
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-08-30Merge PR #12934: Enrich `evar_map` printer with future goals stackPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-29Merge PR #12929: Make abstract compatible with mangle namesPierre-Marie Pédrot
Reviewed-by: jashug Reviewed-by: ppedrot
2020-08-29Merge PR #12939: Fix configure check for zarithcoqbot-app[bot]
Reviewed-by: gares
2020-08-29Fix configure check for zarithGaëtan Gilbert
Fix #12938
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: maximedenes Ack-by: SkySkimmer
2020-08-28Merge PR #11742: [numeral] [plugins] Remove Coq's `Bigint` module in favor ↵coqbot-app[bot]
of ZArith. Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: liyishuai Ack-by: MSoegtropIMC Ack-by: ejgallego Ack-by: maximedenes Ack-by: proux01 Ack-by: vbgl
2020-08-28Merge PR #12933: Add test for past anomalyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-28Merge PR #12932: par: print relevant subgoal when failingcoqbot-app[bot]
Reviewed-by: gares
2020-08-28Drop opaque bodies of abstracted definitions.Pierre-Marie Pédrot
This should save us a lot of useless hashconsing. This change should not be observable because outside of the proof, the abstracted definition will be either inlined or redefined with the body coming from the side-effect.
2020-08-28Enrich `evar_map` printer with future goals stackMaxime Dénès
This is a useful for debugging.
2020-08-28Name saved goals in name_mangling testGaëtan Gilbert
Should be more robust with async proofs
2020-08-28Clarify variable names in abstract implementationGaëtan Gilbert
It makes no sense to call the context from the goal "global"
2020-08-28Make abstract compatible with mangle namesGaëtan Gilbert
Fix #12928 Fix #3146
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 06:52:57 +0000