aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
| | | | | | | | | | | | | | | | | | | | | | | Inner sub-modules with "Definition t := t" is hard to handle by extraction: "type t = t" is recursive by default in OCaml, and the aliased t cannot easily be fully qualified if it comes from a higher unterminated module. There already exists some workarounds (generating Coq__XXX modules), but this isn't playing nicely with module types, where it's hard to insert code without breaking subtyping. To avoid falling too often in this situation, I've reorganized: - GenericMinMax : we do not try anymore to deduce facts about min by saying "min is a max on the reversed order". This hack was anyway not so nice, some code was duplicated nonetheless (at least statements), and the module structure was complex. - OrdersTac : by splitting the functor argument in two (EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid the need for aliasing the type t, cf NZOrder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16100 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
| | | | | | | hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making subset_eq_compat applying over more general domain "Type" (see #2938).Gravatar herbelin2012-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Identities over types satisfying Uniqueness of Identity ProofsGravatar herbelin2012-12-04
| | | | | | | | | | themselves satisfied Uniqueness of Identity Proofs. Otherwise said uniqueness of equality proofs is enough to characterize types whose equality has a degenerated "homotopical" structure (this is a short proof of a result inspired by Voevodsky's proof of inclusion of h-level n into h-level n+1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Isolating the ingredients of the proof of Prop<>Type (r15973). SeeingGravatar herbelin2012-11-15
| | | | | | | it as a consequence of the derivability of Hurkens' paradox in the presence of a retract from Type to Prop. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some lemmas on property of rewriting. It will probably be worth atGravatar herbelin2012-11-15
| | | | | | | some time to provide a library stating the groupoid structure of equality proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a proof that Prop<>Type, for arbitrary fixed Type.Gravatar herbelin2012-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15973 85f007b7-540e-0410-9357-904b9bb8a0f7
* A decidability property of functional relations over decidable codomains.Gravatar herbelin2012-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15972 85f007b7-540e-0410-9357-904b9bb8a0f7
* For the record, two examples of short proofs of uniqueness of identityGravatar herbelin2012-11-15
| | | | | | proofs, on bool and nat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
| | | | | | | | | | | | | instead of a general constr: this is the most common case and does not loose generality (one can simply define constrs before Hint Resolving them). Benefits: - Natural semantics for typeclasses, not class resolution needed at Hint Resolve time, meaning less trouble for users as well. - Ability to [Hint Remove] any hint so declared. - Simplifies the implementation as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed a few calls to "Opaque" in Logic.v ineffective since at leastGravatar herbelin2012-10-24
| | | | | | V7.1. Thanks to Assia for reporting. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing redundant definition of case_eq (see #2919).Gravatar herbelin2012-10-16
| | | | | | Thanks to F. Blanqui for spotting it out. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "En cours pour 'generalize in clause' et 'induction in clause'"Gravatar herbelin2012-10-04
| | | | | | Sorry, was committed mistakenly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15856 85f007b7-540e-0410-9357-904b9bb8a0f7
* En cours pour 'generalize in clause' et 'induction in clause'Gravatar herbelin2012-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15838 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetRBT: a tail-recursive plengthGravatar letouzey2012-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Same for FinGravatar pboutill2012-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vector equalities first stuffGravatar pboutill2012-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
| | | | | | | | | | | | After discovering a rewrite in Ergo that takes a loooong time due to a bad interaction with the instances of Permutation and PermutationA : - PermutationA is now in a separate file SetoidPermutation - File Permutation.v isn't Require'd by SetoidList anymore nor MergeSort.v, just the definitions in Sorted.v - Attempt to put a priority on these instances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
| | | | | | | | | | | | | | | | | | The ugly syntax "destruct x as [ ]_eqn:H" is replaced by: destruct x eqn:H destruct x as [ ] eqn:H Some with induction. Of course, the pattern behind "as" is arbitrary. For an anonymous version, H could be replaced by ?. The old syntax with "_eqn" still works for the moment, by triggers a warning. For making this new syntax work, we had to change the seldom-used "induction x y z using foo" into "induction x, y, z using foo". Now, only one "using" can be used per command instead of one per comma-separated group earlier, but I doubt this will bother anyone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Two adaptations after the changes of level of ->Gravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15541 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore the compatibility notation Compare.not_eq_symGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
| | | | | | | | | One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup in recent proofs concerning piGravatar letouzey2012-07-05
| | | | | | | | Initial idea was to just avoid compat notations such as Z_of_nat --> Z.of_nat, but I ended trying to improve a few proofs... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15520 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetRBT : elementary arith proofs instead of calls to liaGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15519 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | | | | | Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ↵Gravatar pboutill2012-06-20
| | | | | | patch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2695: infinite loop in dependent destruction.Gravatar msozeau2012-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15451 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinInt: a forgotten scope for a notationGravatar letouzey2012-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15450 85f007b7-540e-0410-9357-904b9bb8a0f7
* These files are displaced from Rtrigo.v and Ranalysis_reg.vGravatar bertot2012-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15430 85f007b7-540e-0410-9357-904b9bb8a0f7
* finish the rearrangement for removing the sin_PI2 axiom. This new versionGravatar bertot2012-06-11
| | | | | | | | | | | | | | | - provides the atan function - shows that this function is equal between -1 and 1 to a function defined with power series - establishes the equality with the PI value as given by the alternated series constructed with PI_tg - provides a smarter theorem to compute approximations of PI, based on a formula in the same family as the one used by John Machin in 1706 Dependencies between files have been rearranged so that the new theorems are loaded with the library Reals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds the proof of PI_ineq, plus some other smarter ways to approximate PIGravatar bertot2012-06-11
| | | | | | | and of course, the definition of atan (the inverse of tan, from R to (-PI/2, PI/2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications and rearrangements to remove the action that sin (PI/2) = 1Gravatar bertot2012-06-05
| | | | | | Beware that the definition of PI changes in the process git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15425 85f007b7-540e-0410-9357-904b9bb8a0f7
* list_eq_dec now transparent (wish #2786)Gravatar letouzey2012-06-01
| | | | | | | The proof is also replaced by a mere "decide equality". Patch by Robbert Krebbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Functions *_beq aren't generated anymore, remove comments about themGravatar letouzey2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs revealed by playing with contribsGravatar pboutill2012-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Permutation: remove a compatibility notation which doesn't help MathClassesGravatar letouzey2012-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15341 85f007b7-540e-0410-9357-904b9bb8a0f7
* SetoidList: explicit the fact that InfA_compat won't use ltA_strorderGravatar letouzey2012-05-22
| | | | | | | | For that, we use the new "Proof using ...". This way, we're sure that a later change in the behavior of intuition or any other tactics will not create an artificial dependency again (cf. r15180). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15340 85f007b7-540e-0410-9357-904b9bb8a0f7
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
| | | | | | | | | | In particular, characterisation of NoDup and Permutation in term of nth_error and nth Some of these results have been suggested last year by Bas Spitters (cf. MathClasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
| | | | | | | | Let's check tomorrow the impact on contribs: are the recent build failures related to the "not" unfolding stategy or to the new handling of conjonction-like constructors ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vectors takes advantage of pattern matching compiler fixupGravatar pboutill2012-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2767Gravatar pboutill2012-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15291 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 15:09:27 +0000