aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
| | | | replacement for 8.4's "Require Omega").
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
| | | | Closes #57.
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* Add some missing Proof keywords.Gravatar Guillaume Melquiond2015-03-06
|
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
|
* MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
|
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
| | | | | | | | | | | | | | | | | | | | | | NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
* Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
| | | | | | | | | This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035.
* Reorder the steps of the easy tactic. (Fix for bug #2630)Gravatar Guillaume Melquiond2015-02-25
| | | | | | | Due to the way it was laid out, the tactic could prove neither (Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True) yet it could prove (Zle x x /\ True) and (P /\ Q |- P).
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
|
* Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
|
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
| | | | generalizing * which was broken since 8.4.
* There was one more universe needed due to the use of now ↵Gravatar Matthieu Sozeau2015-01-18
| | | | | | non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again.
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| | | | | | | | | | definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions.
* Remove typeclass opaque directive, some proofs in the stdlib rely on it ↵Gravatar Matthieu Sozeau2015-01-15
| | | | being transparent
* Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-15
| | | | | | Off by default as it can be backwards-incompatible (e.g. produces loop in the library without an additional Typeclasses Opaque directive in RelationPairs).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ↵Gravatar Arnaud Spiwack2014-12-28
| | | | | section variable. For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
| | | | | | | Fixes #3379 and part of #3363. Also avoids fragile code propagating required libraries when closing an interactive module. Had to fix a few occurrences in std lib.
* Adds two lemmas about hderror to the List standard library.Gravatar Sébastien Hinderer2014-12-18
|
* Implement the nodup function on lists and prove associated results.Gravatar Sébastien Hinderer2014-12-18
|
* Lists: enhanced version of Seb's last commit on Exists/ForallGravatar Pierre Letouzey2014-12-18
|
* Lists: a few results on Exists and Forall and a bit of code cleanup.Gravatar Sébastien Hinderer2014-12-18
|
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
| | | | | | | + consequences of this check on the standard library (moved the no-op in Notation modifiers to what there were supposed to do; these are anyway local notations, so compatibility is safe - please AS or PL, amend if needed).
* List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Gravatar Pierre Letouzey2014-12-11
|
* First series of results on lists.Gravatar Sébastien Hinderer2014-12-11
|
* Added an arithmetical characterization of the hypothesis of WKL.Gravatar Hugo Herbelin2014-12-01
|
* Clarifying the role of ListSet.v in the library, compared to otherGravatar Hugo Herbelin2014-11-18
| | | | finite set libraries.
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
| | | | local definitions...
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
|
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
|
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
|
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
|
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
|
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
|
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une ↵Gravatar Hugo Herbelin2014-10-17
| | | | | | équation;" which was committed by mistake. This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
|
* ConstructiveEpsilon: simplify the before_witness type using non-uniform ↵Gravatar Arnaud Spiwack2014-10-16
| | | | parameters.
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
| | | | | | | for the record binder of classes. This name is no longer generated in the kernel but part of the declaration. Also cleanup the interface to recognize primitive records based on an option type instead of a dynamic check of the length of an array.
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
| | | | | projections and regular records. Easily fixable backwards incompatibility.
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
| | | | Thanks to Yves for reporting it!
* eta contractionsGravatar Pierre Boutillier2014-10-01
|
* argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlGravatar Pierre Boutillier2014-10-01
|
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
|
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | (but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on.
* Hurkens.v: Fix a syntax error.Gravatar Arnaud Spiwack2014-09-26
| | | Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
* ClassicalFacts: adds a proof that weak excluded middle implies weak proof ↵Gravatar Arnaud Spiwack2014-09-26
| | | | | irrelevance. Application of previous commit in Hurkens.v.
* Hurkens.v: new paradox: type of modal propositions is not a retract.Gravatar Arnaud Spiwack2014-09-26
| | | In particular there is no retract of the type of negative propositions in a negative proposition.
* Hurkens.v: fix coqdoc formatting in a comment.Gravatar Arnaud Spiwack2014-09-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 13:31:36 +0000