aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-07-05Further cleanup of dead code in the Reductionops API.Pierre-Marie Pédrot
2020-07-05Remove the last use of the Stack module in Tacred.Pierre-Marie Pédrot
2020-07-05Inline make_elim_fun in Tacred.Pierre-Marie Pédrot
We seize the opportunity to simplify the code and hoist out computations that can be avoided.
2020-07-05Inline the Reductionops.fix_recarg function.Pierre-Marie Pédrot
It was only used in Tacred, and with a type that forced to perform a change of representation of stacks.
2020-07-05Inline mutual recursion helpers in simpl implementation.Pierre-Marie Pédrot
This highlights static invariants about the function.
2020-07-05Stop back-and-forth array to list conversions in simpl.Pierre-Marie Pédrot
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
Reviewed-by: ppedrot
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-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-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-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
2020-07-01Merge PR #12605: [test-suite] async-proofs off in tests with Fail TimeoutGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-01Merge PR #12615: [ci] [performance-tests] Use a lighter target.Gaëtan Gilbert
Reviewed-by: JasonGross Reviewed-by: SkySkimmer
2020-07-01Use weak ref to memoize Evarutil.is_ground_envGaëtan Gilbert
2020-07-01Merge PR #12616: [ci] Disable the OCaml 4.12 targetGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-01[ci] Disable the OCaml 4.12 targetEmilio Jesus Gallego Arias
Recent changes in Coqbot plus the unfortunate breakage OCaml upstream has make this too noisy. We will re-enable once https://github.com/ocaml/dune/pull/3585 is accepted upstream.
2020-06-30Cleanup mentions of -as in coqdep usage messageGaëtan Gilbert
2020-06-30[ci] [performance-tests] Use a lighter target.Emilio Jesus Gallego Arias
The current `perf` CI target is quite heavy, failing from out of memory sometimes. We use the target suggested by Jason Gross (<- thanks) in https://github.com/coq/coq/pull/12577#issuecomment-651970064
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
Now that `Printmods` is above `Declaremods`, we don't need to pass the extra `mod_ops` argument.
2020-06-30[states] Move States to vernacEmilio Jesus Gallego Arias
We continue to push state layers upwards, in preparation of a functional vernacular interpretation. Now we move `States` and `Printmod` which messes with the global state as to temporarily create envs with modules.
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic ↵Emilio Jesus Gallego Arias
definitions Reviewed-by: ejgallego Reviewed-by: herbelin
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
Apparently the `Timeout` exception is raised by a signal handled, and that can happen when the running thread is a worker manager, rather than the main thread (the one that should be interrupted). Given that the point of these tests is to test *auto and not the STM, we disable async proofs forcibly.
2020-06-29Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-29Adding overlay.Pierre-Marie Pédrot
2020-06-29Refining out the Refiner.Pierre-Marie Pédrot
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-29Remove the deprecated functions from refiner, moving them to Tacticals.Pierre-Marie Pédrot
2020-06-29Merge PR #12604: Update CAMLDONTLINK in CoqMakefile.inEnrico Tassi
Reviewed-by: gares
2020-06-29Merge PR #12372: [declare] Refactor constant information into a record.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-28Update CAMLDONTLINK in CoqMakefile.inAndres Erbsen
I used SYSMOD from Makefile.build as the ground truth.
2020-06-27Merge PR #12518: [ci] [ocaml] Track OCaml 4.12Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-27Merge PR #12583: [test-suite] Fix dependencies of modules/ filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-26Merge PR #12598: Mention VSCoq with respect to _CoqProjectThéo Zimmermann
Reviewed-by: Zimmi48
2020-06-26Mention VSCoq with respect to _CoqProjectCarl Patenaude-Poulin
2020-06-26[ci] Add overlays for PR #12372Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:52:53 +0000