aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-31Fix load_printers after zarithGaëtan Gilbert
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-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
2020-08-28Adding overlay for coq-elpi.Hugo Herbelin
2020-08-28About: Add a mention that arguments have been renamed, if ever it is the case.Hugo Herbelin
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
2020-08-28Where there are several lists of implicit arguments, don't pretend names matter.Hugo Herbelin
That is, in "About", use _ for the variables of the extra lists. See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.
2020-08-28Do not write "rename" for arguments in About, since these arguments are ↵Hugo Herbelin
validated.
2020-08-28When printing the type in About, use the renamed arguments.Hugo Herbelin
2020-08-28When reporting an implicit argument error on a rename argument, use the ↵Hugo Herbelin
renaming. Example: > Arguments id [B] {b} : rename. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Argument B is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].
2020-08-28In "About", print all arguments, even if it is trailing list of _.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:21:49 +0000