aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
| | | | | | | | | | | - reinstall (x : T | P) binder syntax extension. - fix a wrong Evd.define in coercion code. - Simplify interface of eterm_obligations to take a single evar_map. - Fix a slightly subtle bug related to resolvability of evars: some were marked unresolvable and never set back to resolvable across calls to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Final part of moving Program code inside the main code. Adapted ↵Gravatar msozeau2012-03-14
| | | | | | add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Everything compiles again.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove support for "abstract typing constraints" that requires unicity of ↵Gravatar msozeau2012-03-14
| | | | | | | | | | | solutions to unification. Only allow bidirectional checking of constructor applications, enabled by a program_mode flag: it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated with delta-equivalent but not syntactically equivalent terms. Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vector: missing injection lemmas and better impossible branchesGravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unblocking code in dependent destruction due to zeta being used in ↵Gravatar msozeau2012-02-01
| | | | | | unfold now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Tentative to fix bug #2628 by not letting intuition break records. ↵Gravatar msozeau2012-01-31
| | | | | | | | | Might be too much of a backwards-incompatible change" Indeed it is breaking too many scripts. This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14956 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative to fix bug #2628 by not letting intuition break records. Might be ↵Gravatar msozeau2012-01-28
| | | | | | too much of a backwards-incompatible change git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14949 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ↵Gravatar msozeau2012-01-28
| | | | | | #2674) and properly clear [block] at end of simplification (bug #2691). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deleted the only use of BeginSubProof from the standard library.Gravatar ppedrot2012-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14938 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more use of tauto in Init/Gravatar pboutill2012-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14918 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetAVL: better implementation of filter suggested by X. LeroyGravatar letouzey2012-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the decidability of (<=) on nat.Gravatar ppedrot2012-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14896 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the itarget of the previous commit...Gravatar ppedrot2012-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a typeclass-based system to reason on decidable propositions.Gravatar ppedrot2012-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
| | | | | | | unfolded fixpoints when calling destruct). However, this might break compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vectors use a bit more the pattern matching compilerGravatar pboutill2011-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14773 85f007b7-540e-0410-9357-904b9bb8a0f7
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
* VectorDef.v takes benefit of dependencies being taken into accountGravatar herbelin2011-11-21
| | | | | | | | | | between initial terms to match in pattern-matching compilation algorithm. Also simplified Fin.v though the simplification was possible beforehand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
| | | | | | | | | | | | | | This adds two experimental features to the typeclass implementation: - Path cuts: a way to specify through regular expressions on instance names search pathes that should be avoided (e.g. [proper_flip proper_flip]). Regular expression matching is implemented through naïve derivatives. - Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no longer applied backwards, but introducing a specific [Equivalence] in the environment register a [Reflexive] hint as well. Currently not backwards-compatible, the next patch will allow to specify direction of subclasses hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning a little bit the files talking about descriptions: avoidingGravatar herbelin2011-11-03
| | | | | | | same name for different statements as noticed by Adam Chlipala on coq-club, avoiding stating the same axiom twice in distinct files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).Gravatar herbelin2011-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).Gravatar herbelin2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Equality.injectable which did not detect an equality withoutGravatar herbelin2011-10-22
| | | | | | | | | | | | | | | constructors as non relevant for injection. Also made injection failing in such situation. Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases (observed in the compilation of CoinductiveReals.LNP_Digit). The most probable explanation is that this loop was formerly protected by a failing rewrite which stopped failing after revision 14549 made second-order pattern-matching more powerful. Also suppressed dead code in Invfun.intros_with_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing ↵Gravatar msozeau2011-10-17
| | | | | | zeta reductions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14564 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightGravatar letouzey2011-10-14
| | | | | | | | | | | In fact, this formula "fold ... = fold_right ... (rev (elements))" was already frequently used, but without ever stating it explicitely. Instead, we were always chaining two rewrites each time. Thanks to A. Appel for mentionning this question of fold_right vs. fold_left in the spec of fold. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proper fix for complement/flip instances.Gravatar msozeau2011-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14533 85f007b7-540e-0410-9357-904b9bb8a0f7
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
| | | | | | Btw, we also get rid of equalities on something else than elements or sets git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14525 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved handling of element equalities in fsetdec (fix #2467)Gravatar letouzey2011-10-07
| | | | | | | | | | | - We now handle things like (H : E.eq x x -> ...) by rewriting E.eq x x into True. - There was also a confusion between E.t and its various equivalent (but syntactically different) forms. This should be solved by preventing inlining during an inner functor application. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing vernacular code mistakenly committed.Gravatar herbelin2011-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use an ad-hoc monomorphic list in RelationClasses to avoid some universe ↵Gravatar letouzey2011-10-05
| | | | | | | | constraints Patch by Robbert Krebbers (cf. #2611) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14509 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving never-used comments from Zhints.v to dev/doc so as not toGravatar herbelin2011-10-01
| | | | | | obfuscate the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Euclid: make the proof transparent (example of extraction in stdlib)Gravatar letouzey2011-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Omega: for non-arithmetical goals, try proving False from context (wish #2236)Gravatar letouzey2011-09-16
| | | | | | | | | | | | | | | | | | This way, no more error messages like "Unrecognized predicate". Some code simplification and reorganization on the way, in particular a few tests like "is_Prop ..." or "closed0 ..." were actually useless. Also add support for the situation H:~Zne x y for uniformity. Beware: scripts relying negatively on the strength of omega may have to be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails."). For instance, one line deletion in PermutSetoid.v Probably more cumbersome : "auto with *" becomes stronger since it may call omega. Todo : check the impact on contribs tomorrow. Btw, this commit seems to solve a bug where omega was to be guided by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid registering λ and Π as keywords just for some private Local NotationGravatar letouzey2011-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2589: Documentation patch of Hendrik TewsGravatar pboutill2011-09-02
| | | | | | + s/cbv/lazy of bug 2542 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use of the standard terminology for Diaconescu's theorem (not "paradox").Gravatar herbelin2011-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Give inner fixpoint of gcd31 a name, to avoid excessive unfoldingGravatar glondu2011-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Smaller proof terms for QcPower_{0,pos}Gravatar glondu2011-08-17
| | | | | | | The use of compute produces huge terms that contain hundreds of unfolded Zadd, Zmul, Zsucc! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14412 85f007b7-540e-0410-9357-904b9bb8a0f7
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
| | | | | | | | | | | | | | | | | | | | | | | | Instead of hard-coding in search.ml some substrings such as "_admitted" or "_subproof" we don't want to see in results of SearchAbout and co, we now have a user command: Add Search Blacklist "foo". Remove Search Blacklist "foo". (* the opposite *) Print Table Search Blacklist. (* the current state *) In Prelude.v, three substrings are blacklisted originally: - "_admitted" for internal lemmas due to admit. - "_subproof" for internal lemmas due to abstract. - "Private_" for hiding auxiliary modules not meant for global usage. Note that substrings are searched in the fully qualified names of the available lemmas (e.g. "Coq.Init.Peano.plus"). This commit also adds the prefix "Private_" to some internal modules in Numbers, Z, N, etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take benefit of bullets available by default in PreludeGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | "rewrite Heq in H" but "rewrite" is sometimes used by users and I don't want to have to change their file. The solution to put the notations in a module does not work with name "rewrite" because loading the module would change the status of "rewrite" from simple ident to keyword (and we cannot declare "rewrite" as an ident, as shown in previous commit). Then we come back on notation "rew" (this name is also used by some users), in a module. This continues commit r14366 and r14390 and improves on the level of the notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14400 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinInt: more structured scripts thanks to bullets and { }Gravatar letouzey2011-08-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ↵Gravatar aspiwack2011-08-09
| | | | | | so that the files in Init can benefit from the full-blown tactic language. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14392 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some forgotten lemma in Arith with "O" in the name instead of "0".Gravatar herbelin2011-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14391 85f007b7-540e-0410-9357-904b9bb8a0f7
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
| | | | | | a smaller risk that "rewrite" clashes with a name used for constr). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14390 85f007b7-540e-0410-9357-904b9bb8a0f7
* All the parameters of Compare are implicits.Gravatar pboutill2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14297 85f007b7-540e-0410-9357-904b9bb8a0f7
* All the parameters of or can be implicits.Gravatar pboutill2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14296 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 16:34:55 +0000