aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-08-09Add a changelog entryKazuhiko Sakaguchi
Acknowledgement: This work is financially supported by Peano System Inc. on-behalf-of: @peano-system <info@peano-system.jp>
2019-08-09Overlay for #10642Gaëtan Gilbert
2019-08-09Recommend assigning an issue before fixing a bug.Théo Zimmermann
Contributors with write-access can now assign people who commented an issue: https://github.blog/changelog/2019-06-25-assign-issues-to-issue-commenters/
2019-08-09Merge PR #10641: Fix regression of #10637 (-emacs arg should set color to ↵Emilio Jesus Gallego Arias
`EMACS) Reviewed-by: ejgallego
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
This lets us remove the passing around of "status" in comassumption and generally makes highlighting axiom adding lines in coqide more reliable as there's no need for per-command code. If a command adds multiple axioms it will emit AddedAxiom multiple times, this doesn't seem to be a problem though. We may wonder if "Fail Fail Axiom" should be highlighted as "Axiom" (both before and after this commit it is).
2019-08-08Merge PR #10639: map directory read error to empty directoryEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-08-08Fix namespace of Cauchy realsVincent Semeria
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵Maxime Dénès
involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ↵Vincent Semeria
Cauchy reals
2019-08-08map directory read error to empty directoryspanjel
2019-08-08[doc][ssr][under][setoid] Add changelog entryErik Martin-Dorel
2019-08-08[ssr] under: Add a contrived example to test under/over with SetoidsErik Martin-Dorel
* Borrow ideas from the Setoid refman documentation: https://coq.inria.fr/refman/addendum/generalized-rewriting.html#first-class-setoids-and-morphisms * Introduce a relation with the following signature: [Rel : forall (m n : nat) (s : Setoid m n), car s -> car s -> Prop]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 14:48:45 +0000