aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-07-17Tweak the warning for arbitrary term hints.Pierre-Marie Pédrot
Fixes #11970.
2020-07-16Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2020-07-16Merge PR #12675: Don't catch anomalies for evarconv "cannot find an ↵Emilio Jesus Gallego Arias
instance" error Reviewed-by: ejgallego
2020-07-15Merge PR #12671: Minor improvement to CI logsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-15Merge PR #12673: Fix fiat_crypto(_ocaml) needs/dependenciesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-15Merge PR #12692: Compatibility of make-change-log with MacOS X whose "sed" ↵Emilio Jesus Gallego Arias
does not support the "\+" operator of regular expressions Reviewed-by: ejgallego
2020-07-15Compatibility of make-change-log with MacOS X whose "sed" does not support "\+".Hugo Herbelin
We make it compatible by expanding "[0-9]\+" into "[0-9][0-9]*".
2020-07-13Merge PR #12681: tactics.rst: `Require A` is enough for `A`'s hintsThéo Zimmermann
Reviewed-by: Zimmi48
2020-07-13Don't catch anomalies for evarconv "cannot find an instance" errorGaëtan Gilbert
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
As the text says later: > Hints should only be made available when the module they are defined in is imported, not just required.
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject ↵Pierre-Marie Pédrot
entry struc_tuple Reviewed-by: ppedrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-11Merge PR #12635: Correct comment and clarify constantPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-10Merge PR #12638: Some changes of representation in TacredEnrico Tassi
Ack-by: backtracking Reviewed-by: gares
2020-07-10Add changelog.Pierre-Marie Pédrot
2020-07-10Fix #12513: coq no longer reports mismatched version numbers.Pierre-Marie Pédrot
2020-07-10Minor improvement to CI logsGaëtan Gilbert
- don't `set -x` while loading overlays, non-verbose untaring - ls _build_ci to help figure out artifact download issues
2020-07-10Merge PR #12666: Add test for #10890 derive vs abstractEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-10Fix fiat_crypto(_ocaml) needs/dependenciesGaëtan Gilbert
It seems gitlab has issues with missing transitive dependencies, for instance in https://gitlab.com/coq/coq/-/pipelines/164834444 rewriter failed (missing overlay), fiat_crypto was skipped and fiat_crypto_ocaml was incorrectly started and so failed. May also fix (intermittent?) issue where it doesn't download the rewriter or bignum artifact and gets incompatible ocaml when compiling.
2020-07-10Merge PR #12537: Take into account the existing delta-resolver when starting ↵Gaëtan Gilbert
a new interactive module or module type Reviewed-by: SkySkimmer
2020-07-09Merge PR #12542: Defined arbitrary base logarithms (Rlog) and added natural ↵Michael Soegtrop
lemmas to the Real library Reviewed-by: MSoegtropIMC Ack-by: silene
2020-07-09Add test for #10890 derive vs abstractGaëtan Gilbert
2020-07-09Overlay for removing struc_tupleGaëtan Gilbert
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
This requires updating the parameter count at section end, I felt it was easier to do with rebuild_function but it could be done in discharge if needed. Incidentally fixes #12649.
2020-07-09Merge PR #11836: [obligations] Functionalize Program stateGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive ↵Enrico Tassi
projection Reviewed-by: ejgallego Ack-by: gares
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[ci] Overlay for metacoq and rewriterEmilio Jesus Gallego Arias
2020-07-08[declare] Allow obligations update on equations closing hook.Emilio Jesus Gallego Arias
This is also needed in equations.
2020-07-08[obligations] Allow to simultaneously open a proof and add obligationsEmilio Jesus Gallego Arias
2020-07-08[obligations] Allow state-modifying hooksEmilio Jesus Gallego Arias
This is for use in Equations. At some point we should make all hook aware of state, but this should suffice for now. Note the comments as the role of hooks here, this may need further cleanup indeed.
2020-07-08[obligations] Remove duplicate progmap_remove.Emilio Jesus Gallego Arias
This is already taken of by `declare_definition`, by consistency with the mutual case.
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
In our quest to unify all the declaration paths, an important step is to account for the state pertaining to `Program` declarations. Whereas regular proofs keep are kept in a stack-like structure; obligations for constants defined by `Program` are stored in a global map which is manipulated by almost regular open/close proof primitives. We make this manipulation explicit by handling the program state functionally, in a similar way than we already do for lemmas. This requires to extend the proof DSL a bit; but IMO changes are acceptable given the gain. Most of the PR is routine; only remarkable change is that the hook is called explicitly in `finish_admitted` as it had to learn about the different types of proof_endings. Note that we could have gone deeper and use the type system to refine the core proof type; IMO it is still too preliminary so it is better to do this step as an intermediate one towards a deeper unification.
2020-07-08[declare] Generalize type of hooks.Emilio Jesus Gallego Arias
This is essential to allow hooks to modify state.
2020-07-08Adding change log.Hugo Herbelin
2020-07-08Adding test for #12525 (Search of lemmas in Include failing when in Module).Hugo Herbelin
2020-07-08Merge PR #12612: docs(README.md): Update badge and linksEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-08Merge PR #12654: Reindent ppvernac.mlEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-08Merge PR #12645: Cleanup Evarutil APIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-07-08Preserve delta-resolver at Module and Module Type starting.Hugo Herbelin
The default value of the delta-resolver for name aliasing was reinitialized at Module and Module Type starting time. The existing resolver was saved but the saved value was not used in Safe_typing.constant_of_delta_kn_senv and Safe_typing.mind_of_delta_kn_senv. A possible fix could have been to take the saved resolver into account in Safe_typing.constant_of_delta_kn_senv and Safe_typing.mind_of_delta_kn_senv. We just try instead not to reinitialize it. This incidentally fixes #12525 (Search unable to see through an "Include" when in an ongoing "Module").
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_from_context from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_pure_evar_full from the API.Pierre-Marie Pédrot
2020-07-08Small code simplification in Evarutil.new_evar.Pierre-Marie Pédrot
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-07Reindent ppvernac.mlGaëtan Gilbert
It used to be a big functor but changed in 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 The functor indent is now incorrect.
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
Fix #12651
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:06:47 +0000