aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
Exceptions should not printed except for the top-level. There is the weird anomaly-absorbing code in `Reductionops`, I wonder how frequent that case is, but as the exception is absorbed printing there could have a real impact.
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-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-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-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-06Merge PR #12622: Use goal cycling instead of manual evar generation order in ↵Gaëtan Gilbert
internal_cut_rev Reviewed-by: SkySkimmer
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
Perhaps we should thread an evar map with the Var universes added through to cs_pattern_of_constr but that would be significantly more invasive. Fix #12528
2020-07-05Merge PR #12641: Windows build: use architecture dependent version of windresEnrico Tassi
Reviewed-by: gares
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: gares
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-04Windows build: remove patch for windres architectureMichael Soegtrop
2020-07-04Windows build: use architecture dependent version of windresMichael Soegtrop
2020-07-03Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in ↵Gaëtan Gilbert
custom gr… Reviewed-by: SkySkimmer Ack-by: ejgallego Ack-by: herbelin
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2020-07-02Merge PR #12628: Fix debug printer for auctx in presence of AnonymousEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-02Merge PR #12614: Cleanup mentions of -as in coqdep usage messageEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-02Fix debug printer for auctx in presence of AnonymousGaëtan Gilbert
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
Fix #12551
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵Gaëtan Gilbert
patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2020-07-02Merge PR #12620: [state] Consolidate state handling into VernacstateGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-07-02Merge PR #12618: Use weak ref to memoize Evarutil.is_ground_envPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-01Use goal cycling instead of manual evar generation order in internal_cut_rev.Pierre-Marie Pédrot
This reduces the combinatorial complexity of the function, and the code size as well.
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
After #12504 , we can encapsulate and consolidate low-level state logic in `Vernacstate`, removing `States` which is now a stub. There is hope to clean up some stuff regarding the handling of low-level proof state, by moving both `Evarutil.meta_counter` and `Evd.evar_counter_summary` into the proof state itself [obligations state is taken care in #11836] , but this will take some time.
2020-07-01Add a changelog.Pierre-Marie Pédrot
2020-07-01Add a test for Ltac2 parsing of parameterized types.Pierre-Marie Pédrot
2020-07-01Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.Pierre-Marie Pédrot
It seems that nobody tried to write a parameterized type with more than one parameter since this was causing a syntax error. LL(1) being great, we work around the issue by factorizing the syntax with the generic parentheses and decide the validity after parsing.
2020-07-01Overlays for UIP in SPropGaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12504: [states] Move States to vernacGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: maximedenes
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:30:16 +0000