aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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]
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
Changes: * Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive]; * Add ssrsetoid.v that links [ssrclasses.Reflexive] and [RelationClasses.Reflexive]; * Add [Require Coq.ssr.ssrsetoid] in Setoid.v; * Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that ports some non-exported material from rewrite.ml; * Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin; * Update doc and tests as well. Summary: * We can now use the under tactic in two flavors: - with the [eq] or [iff] relations: [Require Import ssreflect.] - or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.] (while [ssreflect] does not require [RelationClasses] nor [Setoid], and conversely [Setoid] does not require [ssreflect]). * The file ssrsetoid.v could be skipped when porting under to stdlib2.
2019-08-07[funind] Move some exception-based control flow to explicit option typing.Emilio Jesus Gallego Arias
2019-08-07[funind] Port indfun to the new tactic engine.Emilio Jesus Gallego Arias
2019-08-07Merge PR #10604: Simplify Lib section handlingEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-08-07Merge PR #10525: [funind] Miscellaneous code reorganizations and cleanupPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-06Prove the completeness of real numbers from logical axiom sig_not_decVincent Semeria
2019-08-06[parsing] unify checks for contiguity of tokens in Ltac2 and G_primEnrico Tassi
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
* Add an extra test with an Equivalence. * Update the doc accordingly.
2019-08-06[ssr] export Ssrequality.ssr_is_setoidErik Martin-Dorel
2019-08-06Merge PR #10557: Fixing #10286 (coqide hangs on invalid filenames)Pierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-08-06Merge PR #10618: Add missing *.exe files to "make clean"Enrico Tassi
Reviewed-by: gares
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive ↵Théo Zimmermann
Projection Compatibility Reviewed-by: Zimmi48
2019-08-05Merge PR #10608: Copy edit the Ltac2 documentationJim Fehrle
Reviewed-by: jfehrle Reviewed-by: ppedrot
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-05Merge PR #10585: [coqdoc] Simplify regex for identifiers in commentsVincent Laporte
Reviewed-by: gares Reviewed-by: vbgl
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
Ack-by: Zimmi48 Ack-by: silene
2019-08-05ConstructiveCauchyReals: make explicit structural recursionVincent Laporte
2019-08-04Add missing file ide/default_bindings_src.exe to "make clean"Jim Fehrle
2019-08-04Merge PR #10579: Remove underscores from inserted texts.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-02[lexer]: improve error message on loct_func misuseEnrico Tassi
2019-08-02Merge PR #10543: Remove unused grammar nonterminals and productionsEnrico Tassi
Reviewed-by: ppedrot
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-08-02Merge PR #10553: Use a more traditional definition for uint63_div21 (fixes ↵Maxime Dénès
#10551). Reviewed-by: maximedenes Reviewed-by: proux01
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-31[toplevel] Make all argument lists to be in user-declared order.Emilio Jesus Gallego Arias
As reported by Karl Palmskog, some lists of arguments were supposed to appear in reverse order whereas others do appear in the natural order they are declared. Given that in some cases, such as require, order is quite important, we make the parsing return lists in the right order so clients don't have to care about doing `List.rev`.
2019-07-31Fix #7348: extraction of dependent record projectionsKazuhiko Sakaguchi
- Inline record projections by default (except for Haskell extraction). - Extend `pp_record_proj` for record projections involving `MLmagic`. - Remove special treatments for pretty-printing for record projections other than `pp_record_proj`. - `micromega.ml` had to be changed due to this change of the extraction plugin. Acknowledgement: This work is financially supported by Peano System Inc. on-behalf-of: @peano-system <info@peano-system.jp>
2019-07-31Specialize the section API.Pierre-Marie Pédrot
We split the function used to retrieve the local context from the one used to provide the implicit status of each binder. Most of the users only rely on the former indeed.
2019-07-31Remove the universe part from the section variable mechanism.Pierre-Marie Pédrot
It was factorized away with the universe declaration entry. Actually, pomlymorphic universes were declared twice in Declare, once as a context extension, once as part of the variable itself.
2019-07-31Code simplification in Lib section handling.Pierre-Marie Pédrot
Many invariants were implicit in the code, we make them explicit using dedicated datatypes.
2019-07-31[funind] Remove export of `generate_functional_principle` and `make_scheme`Emilio Jesus Gallego Arias
This removes the export of two internal functions, moving to their only use place. In particular, `make_scheme` was exposing the low-level `proof_entry` object, which should not do. This will allow to refactor all these constant-building functions towards a more uniform use of the API. In particular, all the functions manipulating proof entries directly are in `Gen_principle`.
2019-07-31[funind] Port aux function to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-31[funind] Port invfun to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-31[funind] Move duplicated `observe_tac` function to indfun_common.Emilio Jesus Gallego Arias
We also attempt a version that may work with `Proofview.tactic` , may need more work.
2019-07-31[funind] Move common `make_eq` to funind_common.Emilio Jesus Gallego Arias
2019-07-31[funind] Move principle generation to its own file.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-28 05:04:10 +0000