aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09Merge PR #6155: Get rid of ' notation for Zpos in QArithMaxime Dénès
2018-03-09Merge PR #6937: Add empty compat file for Coq 8.8Maxime Dénès
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-07Add empty compat file for Coq 8.8Jason Gross
This closes #6598
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Remove all uses of Focus in standard library.Théo Zimmermann
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
Fix new deprecation warnings in the standard library.
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5.
2018-02-28Uniform spacing layout in Tactics.v.Hugo Herbelin
2018-02-28Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Hugo Herbelin
2018-02-28Merge PR #6852: [stdlib] move “Require” out of sectionsMaxime Dénès
2018-02-28Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-27[stdlib] move “Require” out of sectionsVincent Laporte
2018-02-24Add String.concatJason Gross
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-21Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predMaxime Dénès
2018-02-20Decimal goodies : conversion to/from Coq stringsPierre Letouzey
Just because it's fun and easy. Not used by the Numeral Notation command.
2018-02-20Decimal: proofs that conversions from/to nat,N,Z are bijectionsPierre Letouzey
2018-02-20Decimal: simple representation of base-10 numbersPierre Letouzey
2018-02-20Trying a hack to support {'pat|P} without breaking compatibility.Hugo Herbelin
Concretely, we bypass the following limitation: The notation "{ ' pat | P }" broke the parsing of expressions of the form "{ forall x, P } + { Q }". Indeed the latter works thanks to a tolerance of Camlp5 in parsing "forall x, P" at level 200 while the rule asks to actually parse the interior of "{ ... }" at level 99 (the reason for 99 is to be below the rule for "M : T" which is at level 100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke the tolerance for constr at level 200. We fix this by adding an ad hoc rule for "{ binder_constr }" in the native grammar (g_constr.ml4). Actually, this is inconsistent with having a rule for "{ constr at level 99 }" in Notations.v. We should have both rules in Notations.v or both rules hard-wired in the native grammar. But I still don't know what is the best decision to take, so leaving as it at the current time. Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in metasyntax.ml (no need to ensure that the rule exist). Disadvantages: if one wants a different initial state without the business needing the "{ }" for sumbool, sumor, sig, sigT, one still have the rules there. Advantages of having them in Notations.v: more modular, we can change the initial state. Disadvantages: one would need a new kind of modifier, something like "x at level 99 || binder_constr", with all the difficulty to find a nice, intuitive, name for "binder_constr", and the difficulty of understanding if there is a generality to this "||" disjunction operator, and whether it should be documented or not.
2018-02-20Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Hugo Herbelin
2018-02-20More structured printing in unicode notations for binders.Hugo Herbelin
2018-02-20User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Hugo Herbelin
2018-02-19Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Maxime Dénès
2018-02-12Add notation {x & P} for sigTTej Chajed
Analogous to existing `{x | P}` notation for `sig`, where the type of `x` is inferred instead of specified.
2018-02-12Merge PR #6139: Make list functions returning sumbools transparentMaxime Dénès
2018-01-08Document between and exists_between types.Ismail
2018-01-06Remove dir-locals and ship suggested helper hooks instead.Gaëtan Gilbert
.dir-locals led to issues with unsafe local variable warnings. With this method the user is opting in to running this code so there are no warnings.
2018-01-03Fix core hint database issue #6521Anton Trunov
2017-12-19Fix warning about shadowing a global name.Gaëtan Gilbert
2017-12-14Add named timers to LtacProfJason Gross
I'm not sure if they belong in profile_ltac, or in extratactics, or, perhaps, in a separate plugin. But I'd find it very useful to have a version of `time` that works on constr evaluation, which is what this commit provides. I'm not sure that I've picked good naming conventions for the tactics, either.
2017-12-12Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsMaxime Dénès
2017-12-11Axiom-free proof of eta expansion.Jasper Hugunin
2017-12-09Remove most uses of function extensionality in Program.CombinatorsJasper Hugunin
2017-12-06Additional rewrite lemmas on Ensembles, in Powerset_factsJoachim Breitner
2017-12-01proposed fix for issue #3213: extra variable m in Lt.S_predfredokun
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-15Make list functions returning sumbools transparentTej Chajed
Specifically Exists_dec, Forall_dec, and Forall_Exists_dec.
2017-11-14Get rid of ' notation for Zpos in QArith.Robbert Krebbers
2017-10-27Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulMaxime Dénès
2017-10-27Chaining two tactics in a proofRaphaël Monat
2017-10-25Moving from `is_true` to `= true`Raphaël Monat
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:10:32 +0000