aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-08-23Merge PR #10686: DAG-style pipelinesGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-08-23[gitlab/ci] Rework stages, always use needs keyword.Théo Zimmermann
Now everything that does not have any dependencies goes to the first stage. The rest goes to the first stage following all its dependencies. All jobs specifying a dependencies keyword also specify a needs keyword.
2019-08-23Merge PR #10691: [doc] Fix documentation of schedule-vioThéo Zimmermann
Reviewed-by: Zimmi48
2019-08-23Create a maintainer team for the contributing process files.Théo Zimmermann
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
Master version of the fix for #10679
2019-08-22[gitlab/ci] Do not wait for all builds to finish to run the tests.Théo Zimmermann
2019-08-22[gitlab/ci] Build Bignums only once.Théo Zimmermann
We go back to the kind of workflow we had in CircleCI thanks to GitLab 12.2 new needs keyword.
2019-08-22[gitlab/ci] Deploy sooner thanks to new needs keyword.Théo Zimmermann
2019-08-22Merge PR #10515: [dune] Move to Dune 1.10, use coq.pp directive.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-08-22Merge PR #9062: Delay the computation of frozen evars in legacy unification.Matthieu Sozeau
Reviewed-by: mattam82
2019-08-22[dune] Move to Dune 1.10, use coq.pp directive.Emilio Jesus Gallego Arias
We use the `(coq.pp ...)` dune directive which will produce correct error messages for `.mlg` files. Unfortunately we cannot yet use the automatic opam generation features of Dune 1.10, as this does require a fully native Dune build. Dune 1.6-1.10 has quite a few other improvements that could be used by Coq, for example for promote modes. I have fixed a couple of documentation issues. `Drop` and `ocamldebug` have been tested in this version.
2019-08-21Merge PR #10678: [ci] Remove dead code.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-21Merge PR #10666: [api] Move `Keys` to pretypingEnrico Tassi
Reviewed-by: gares Reviewed-by: ppedrot
2019-08-20[ci] Remove dead code.Théo Zimmermann
TLC and CPDT are not actually tested. No point in keeping them as if they were.
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-19Merge PR #10672: Std++, Iris, and Lambda-Rust have moved.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-19Merge PR #10671: Remove links to doc artifacts and replace them with the ↵Emilio Jesus Gallego Arias
deployed versions. Reviewed-by: ejgallego
2019-08-19[declare] Use `binding_kind` for implicit kind instead of boolean.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function.
2019-08-19Remove links to doc artifacts and replace them with the deployed versions.Théo Zimmermann
2019-08-19Std++, Iris, and Lambda-Rust have moved.Théo Zimmermann
We update the URLs to the new ones, even if the previous continue to work.
2019-08-19Merge PR #10454: [vernac] Refactor control attributes and fix bug #10452Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-08-19[pcoq] Remove unneeded casting operators.Emilio Jesus Gallego Arias
2019-08-19[parsing] Move pcoq-specific parts in extend to pcoq.Emilio Jesus Gallego Arias
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
This file is unrelated to library, but to pretyping/unification. This commit, along with others already submitted go towards the goal of `library` containing only the handling of library objects.
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
This source of slowness has been observed in VST, but it is probably pervasive. Most of the unification problems are not mentioning evars, it is thus useless to compute the set of frozen evars upfront. We also seize the opportunity to reverse the flag, because it is always used negatively.
2019-08-16Merge PR #10663: Fix quoting in 8.9 changelog entry.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Fix typing_flags in the checkerSimonBoulier
Now all relevant typing_flags are taken in account by the checker. The different forms of assumptions are now printed by the checker.
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
type-in-type universes
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-16Add a file for typing_flags in the test-suite.SimonBoulier
2019-08-16Improve [Print Assumptions] for type-in-type and assumed positive.SimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-08-16Add [Print Typing Flags] command.SimonBoulier
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for ↵SimonBoulier
(co)fixpoints) and [check_positive] (for (co)inductive types).
2019-08-16Apply suggestions from code reviewOliver Nash
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-08-16New lemmas for List.vOliver Nash
* filter_app (moved from MSets/MSetRBT.v) * filter_map * filter_ext_in * ext_in_filter * filter_ext_in_iff * filter_ext * concat_filter_map * combine_nil * combine_firstn_l * combine_firstn_r * combine_firstn * nodup_fixed_point
2019-08-16Merge PR #10457: Make rewrite use the registered elimination schemesPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-08-14[vernac] Refactor common parts of interp_{,delayed}Emilio Jesus Gallego Arias
This should fix some bugs w.r.t. management of state introduced in
2019-08-14[vernac] Pass control attributes to interpretation of delayed proofs.Emilio Jesus Gallego Arias
Fixes #10452
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
We place control attributes on their own, datatype, similarly to regular attributes. This is a step towards fixing #10452 , as we can now decouple control attributes from the vernac AST itself, allowing to pass them independently.
2019-08-14Merge PR #10642: Emit Feedback.AddedAxiom in Declare instead of higher layersPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
`Mlutil.simpl` and `Mlutil.atomic_eta_red` did some unsound eta-reductions as follows: (fun x0 ... xn => MLexn x0 ... xn) ->eta MLexn. `MLexn` raises an exception thus is not a value in OCaml. So the above simplification may change the behavior of extracted programs. This patch restricts `atomic_eta_red` to eta-redexes whose core is both atomic and value. Acknowledgement: This work is financially supported by Peano System Inc. on-behalf-of: @peano-system <info@peano-system.jp>
2019-08-10Compute (if linear_order_T 0 (IPR 22) (IPR 10) (IPR_pos 10) then true else ↵Vincent Semeria
false).
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-08-09Switch constructive Rlt to sort Type, to make it compute laterVincent Semeria
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-22 03:39:05 +0000