aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-01[ssr] Update doc for under w.r.t. setoid-like relationsErik Martin-Dorel
2019-11-01[ssr] chore: Remove ssrclasses.{ml,mli} (now unneeded)Erik Martin-Dorel
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
(namely, [RewriteRelation]s beyond Equivalence ones) Thanks to @CohenCyril for suggesting this enhancement
2019-10-31[ssr] Refactor/Simplify the implementation of underErik Martin-Dorel
* Preserve the same behavior/interface but merge the two Module Types (UNDER_EQ and) UNDER_REL. * Remove the "Reflexive" argument in Under_rel.Under_rel * Update plugin code (ssrfwd.ml) & Factor-out the main step * Update the Hint (viz. apply over_rel_done => apply: over_rel_done) * All the tests still pass! Credits to @CohenCyril for suggesting this enhancement
2019-10-21chore: Enclose the […get_reflexive_proof_ssr…] call in a ↵Erik Martin-Dorel
try/with->assert false as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise).
2019-10-21docs(changelog): Address @gares' commentErik Martin-Dorel
& Put the changelog entry in the proper folder
2019-09-10feat: Add a rewrite rule (UnderE) to unprotect evars in subgoalsErik Martin-Dorel
E.g., if one wish to instantiate these evars manually, in another way than with reflexivity.
2019-09-10[ssr] Add test "do [under ... do ...] in H"Erik Martin-Dorel
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-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-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-30Merge PR #10594: Fix issue #10593 : Software foundations URL changedEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-07-30Merge PR #10595: [CI/Azure/macOS] Unshallow the homebrew-core repositoryEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-29Use the precondition of diveucl_21 to avoid massaging the dividend.Guillaume Melquiond
All the implementations now return (0, 0) when the dividend is so large that the quotient would overflow.
2019-07-29Add a non-overflow precondition to diveucl_21 to align it on standard ↵thery
implementations.
2019-07-29Add test from #10551.Guillaume Melquiond
2019-07-29Transpose the C code of uint63_div21 to the OCaml implementations.Guillaume Melquiond
2019-07-29Use a more traditional definition for uint63_div21 (fixes #10551).Guillaume Melquiond
2019-07-29[CI/Azure/macOS] Unshallow the homebrew-core repositoryVincent Laporte
2019-07-29Fix issue #10593 : Software foundations URL changedMichael Soegtrop
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel Ack-by: herbelin
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
Reviewed-by: ejgallego Reviewed-by: gares
2019-07-29Merge PR #10581: Remove the tactic wizard, as it has not worked for several ↵Pierre-Marie Pédrot
years and no one complained (fixes #10580). Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-07-29Merge PR #10538: [vernac] [inductive] Remove unused functions/exports.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-27Merge PR #10569: [Int63] Remove redundant misnamed lemma lsr_add_distrHugo Herbelin
Reviewed-by: herbelin Reviewed-by: maximedenes Reviewed-by: silene
2019-07-27[coqdoc] Simplify regex for identifiers in commentsLysxia
2019-07-26Remove unused grammar productionsJim Fehrle
2019-07-26Fix typoVincent Semeria
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one ↵Guillaume Melquiond
complained (fixes #10580).
2019-07-26Remove underscores from inserted texts.Guillaume Melquiond
Underscores are used as prefix for accelerators in gtk. In particular, double underscores are used to escape them. So, when applying a template, underscores should be cleaned from the inserted text.
2019-07-26Merge PR #10563: changed name of cos3PI4 to cos_3PI4 for consistencyMichael Soegtrop
Reviewed-by: MSoegtropIMC
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:44:02 +0000