aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* 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
|
* Hurkens.v: update comments.Gravatar Arnaud Spiwack2014-09-25
|
* Return a Prop not an arbitrary Type, and correct a typo.Gravatar Matthieu Sozeau2014-09-24
|
* Hurkens.v: show proofs in coqdoc.Gravatar Arnaud Spiwack2014-09-24
|
* Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Gravatar Arnaud Spiwack2014-09-24
|
* Hurkens.v: coqdoc documentation.Gravatar Arnaud Spiwack2014-09-24
|
* A new version of Hurkens.v.Gravatar Arnaud Spiwack2014-09-24
| | | | Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
* adds general facts in the Reals library, whose need was detected inGravatar Yves Bertot2014-09-23
| | | | experiments about computing PI
* Change some Defined into Qed.Gravatar Guillaume Melquiond2014-09-17
|
* Add some missing Proof statements.Gravatar Guillaume Melquiond2014-09-17
|
* Change an axiom into a definition.Gravatar Guillaume Melquiond2014-09-17
|
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
| | | | | | | | Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
| | | | | Left a README, just in case someone will discover the remnants of it decades from now.
* Prove forall extensionalityGravatar Jason Gross2014-08-26
|
* sed s'/_one_var/_on/g'Gravatar Jason Gross2014-08-26
| | | | For consistency with ChoiceFacts
* Generalize EqdepFactsGravatar Jason Gross2014-08-26
| | | | | | | | The generalized versions are names *_one_var. We preserve backwards compatibility by defining the old versions in terms of the generalized ones. This closes the rest of Bug 3019, and closes pull request #6.
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
|
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
| | | | | | | | | | | I'm not quite sure why, but I'm pretty sure it's not. Rather, in "allowing for foo" and "allowing to foo", "foo" modifies the sense in which someting is allowed, rather than it being "foo" that's allowed. "Allowing fooing" generally works, though it can sound a bit awkward. "Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always acceptable, in-as-much as it's ok to use "one". I haven't touched the older instances of it in the CHANGES file.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | integrate to "rewrite"?) with the code of "replace". Incidentally, "inversion" relies on dependent rewrite, with an incompatibility introduced. Left-to-right rewriting is now done with "eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The first one reduces to the second one but simpl is not anymore able to reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see Zdigits).
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
| | | | change of printing format of forall (need more thinking).
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
| | | | | | | | | | all the tactics using the constructor keyword in one entry. This has the side-effect to also remove the other variant of constructor from the AST. I also needed to hack around the "tauto" tactic to make it work, by calling directly the ML tactic through a TacExtend node. This may be generalized to get rid of the intermingled dependencies between this tactic and the infamous Ltac quotation mechanism.
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
|
* Improving printing of "[]" (nil) in spite of the risk of collisionGravatar Hugo Herbelin2014-08-05
| | | | with possible further use of token "[]" + slight restructuration.
* Testing beautifying on an example.Gravatar Hugo Herbelin2014-08-05
|
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | hypothesis when using it in apply or rewrite (prefix ">", undocumented), and a modifier to explicitly keep it in induction or destruct (prefix "!", reminiscent of non-linerarity). Also added undocumented option "Set Default Clearing Used Hypotheses" which makes apply and rewrite default to erasing the hypothesis they use (if ever their argument is indeed an hypothesis of the context).
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
|
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
| | | | a dependent elimination principle for Prop arguments.
* Move to a representation of universe polymorphic constants using indices for ↵Gravatar Matthieu Sozeau2014-08-03
| | | | | | | variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside.
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
| | | | | | | This commit should be refactored by Pierre L. if he thinks this should replace the previous version of fold_Equal, for now it is a different lemma fold_Equal2. Same for the Section addded to SetoiList, it should maybe replace the previous one.
* Simplified rect2, it turns out Arthur's trick was not required.Gravatar Maxime Dénès2014-07-22
| | | | Standard library now compiles fully.
* A version of Fin.rect2 that is compatible with the fix of the guard condition.Gravatar Maxime Dénès2014-07-22
| | | | Thanks to Arthur Azevedo de Amorim!
* Fixed proof of irrelevance of le on nat, inspired by theGravatar Maxime Dénès2014-07-22
| | | | corresponding proof in ssreflect.
* Completing c236b51348d2 by fixing EqdepFactsv actually committing theGravatar Hugo Herbelin2014-07-17
| | | | new files (WeakFan.v and WKL.v).
* Added a (constructive) proof of Weak Konig's lemma for decidable trees.Gravatar Hugo Herbelin2014-07-15
| | | | | Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem after all.
* Some basics facts about eq_dep.Gravatar Hugo Herbelin2014-07-15
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 17:40:07 +0000