aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Merge PR #11746: Register commonly used names from the Reals library for plug...Théo Zimmermann
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2020-03-04Add file to register names of reals library used by gappaMichael Soegtrop
2020-03-03[zify] efficiency improvementsFrédéric Besson
2020-02-26Merge PR #11644: Use implicit arguments in notations for eq.Hugo Herbelin
2020-02-26Consolidate int63-related notationsMaxime Dénès
2020-02-25Use implicit arguments in notations for eq.Gaëtan Gilbert
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-08Remove -compat 8.9.Théo Zimmermann
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
2020-02-06replace RList by list RYves Bertot
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-14Merge PR #11249: [stdlib] Additional statements in List.vHugo Herbelin
2020-01-08Avoid hardcoded paths in extractionMaxime Dénès
2020-01-06stdlib List: add [remove'] and [count_occ']Yishuai Li
2020-01-05apply suggestions of @anton-trunovOlivier Laurent
2020-01-05clean some indentationsOlivier Laurent
2019-12-26Add rew dependent NotationsJason Gross
2019-12-24Add statements with output in TypeOlivier Laurent
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-14Being explicit on existence of a remote link.Hugo Herbelin
2019-12-06Merge PR #11127: Added theorem Nat.bezout_comm.Hugo Herbelin
2019-12-06additional statements on flat_mapOlivier Laurent
2019-12-06additional statements on map and ForallOlivier Laurent
2019-12-06integration of statements for nthOlivier Laurent
2019-12-06add elt_eq_unitOlivier Laurent
2019-12-06integration of statements for Exists and ForallOlivier Laurent
2019-12-06integration of list_sum and list_maxOlivier Laurent
2019-12-06integration of statements for repeatOlivier Laurent
2019-12-06integration of statements for NoDupOlivier Laurent
2019-12-06integration of additional statements for inclOlivier Laurent
2019-12-06integration of statements for removeOlivier Laurent
2019-12-06integration of statements for InOlivier Laurent
2019-12-06integration of statements for inclOlivier Laurent
2019-12-06integration of statements for revOlivier Laurent
2019-12-06integration of statements for concat and flat_mapOlivier Laurent
2019-12-06integration of statements for seqOlivier Laurent
2019-12-06integration of statements related to last elementOlivier Laurent
2019-12-06integration of Exists_or and Forall_andOlivier Laurent
2019-12-06redundancy between skipn_node and skipn_allOlivier Laurent
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 01:40:49 +0000