aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-30Merge PR #12952: Fix rendering of -> in micromegacoqbot-app[bot]
Reviewed-by: jfehrle
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-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
2020-08-28Add test for past anomalyGaëtan Gilbert
Close #5703 I have no idea when this got fixed.
2020-08-28par: print relevant subgoal when failingGaëtan Gilbert
Fix (partial) #5502
2020-08-28Merge PR #12924: Remove meta-based refiner code in ssrcoqbot-app[bot]
Reviewed-by: gares
2020-08-28Merge PR #12632: [state] A few nits after consolidation of state.coqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego
2020-08-27[zarith] ChangelogEmilio Jesus Gallego Arias
2020-08-27[nsatz] num → zarithVincent Laporte
2020-08-27[numtok] [zarith] SimplificationsEmilio Jesus Gallego Arias
Suggested by Pierre Roux
2020-08-27[zarith] [notation] Build less intermediate valuesEmilio Jesus Gallego Arias
We could still optimize the functions in that file a bit more if there is need.
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-08-27[state] A few nits after consolidation of state.Emilio Jesus Gallego Arias
We remove some dead aliases and add some documentation to the interface file.
2020-08-27Remove the now unused Evarutil.mk_new_meta function.Pierre-Marie Pédrot
This is legacy engine code that shouldn't have been used for a long time.
2020-08-27Remove a call to the old refiner in ssr.Pierre-Marie Pédrot
2020-08-27Merge PR #12922: Fix .gitignore after the merge of #12849.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-27Fix .gitignore after the merge of #12849.Pierre-Marie Pédrot
A stray generated file was forgotten.
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: silene
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
Reviewed-by: ppedrot Reviewed-by: proux01
2020-08-27Merge PR #12918: tacinterp mini cleanup useless letinPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-27Merge PR #12499: Clean future goalsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-08-27Merge PR #12913: Modify lia to work with -mangle-namescoqbot-app[bot]
Reviewed-by: maximedenes Ack-by: SkySkimmer
2020-08-27Merge PR #12850: Avoid running configure when plugins/ modifiedcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: gares
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ↵coqbot-app[bot]
arguments of notations Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-27Merge PR #12867: Fast freeze summarycoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-27Merge PR #12911: Use the lite variants of performance tests in the bench ↵coqbot-app[bot]
default packages Reviewed-by: JasonGross
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-27Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11Enrico Tassi
Ack-by: chdoc Reviewed-by: gares
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Ack-by: ppedrot
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
We used to be refreshing the names for intros but not using the refreshed names. The same pattern of `intro_using` (which is what `intros ?name` effectively is) messing things up as in coq/coq#12881.
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Add test for #10939Maxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-26Better encapsulation of future goalsMaxime Dénès
We try to encapsulate the future goals abstraction in the evar map. A few calls to `save_future_goals` and `restore_future_goals` are still there, but we try to minimize them. This is a preliminary refactoring to make the invariants between the shelf and future goals more explicit, before giving unification access to the shelf, which is needed for #7825.
2020-08-26Use the lite variants of performance tests in the bench default packages.Pierre-Marie Pédrot
They are much faster and should be as informative as their heavy counterparts. I have been forgetting to do that for a long time already.
2020-08-26Merge PR #12764: A fix and two enhancements of trailing pattern ↵Pierre-Marie Pédrot
factorization in recursive notations Reviewed-by: ppedrot
2020-08-26Merge PR #12904: Move bench job definition to its own filePierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:03:10 +0000