aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Derivation of (exists x : A, P x) -> {x : A | P x} for decidable PGravatar emakarov2007-01-23
| | | | | | | | and countable A. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification redondance Axiome du choix unique/descriptionGravatar herbelin2007-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add f_equal case for 6 arguments.Gravatar msozeau2007-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àGravatar herbelin2006-12-28
| | | | | | | égalité décidable + maj dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de la définition de Pind et Prec par une définitionGravatar herbelin2006-12-28
| | | | | | | | | suggérée par Conor McBride qui ne fait pas intervenir eq_rect et qui permet de montrer "facilement" (mais avec l'axiome K) les équations de réduction de Prec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
| | | | | | | | | maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépendence inutileGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9440 85f007b7-540e-0410-9357-904b9bb8a0f7
* AllÃègement de syntxe suite à l'introduction de l'unif patternGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug nommage Zgt_trans_succGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9438 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction Open Local Scope (Ring)Gravatar bgregoir2006-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixes PR#1269 about function: there is no reason well founded induction isGravatar bertot2006-11-05
| | | | | | limited to only Set and not any type in Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9340 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9319 85f007b7-540e-0410-9357-904b9bb8a0f7
* LegacyRfield was opening R_scopeGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9317 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le caractère ² fait planter make docGravatar notin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement des propriétés générales de BinList dans List et des ↵Gravatar herbelin2006-10-26
| | | | | | | | | tactiques de BinList dans un nouveau ListTactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9290 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups, ne chargeait pas les bons fichiersGravatar letouzey2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9278 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la tactique 'remember'Gravatar herbelin2006-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noms "canoniques" pour certaines des propriétés de xor.Gravatar herbelin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du théorème mult_minus_distr_lGravatar notin2006-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9237 85f007b7-540e-0410-9357-904b9bb8a0f7
* revert, the previous commit was a mistakeGravatar bertot2006-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9214 85f007b7-540e-0410-9357-904b9bb8a0f7
* A version of natprering that should be more efficient and removal of a badGravatar bertot2006-10-05
| | | | | | comment in newring.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9212 85f007b7-540e-0410-9357-904b9bb8a0f7
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynomGravatar barras2006-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9210 85f007b7-540e-0410-9357-904b9bb8a0f7
* args implicites dans FieldGravatar barras2006-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9192 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation de RealFieldGravatar barras2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit de field + renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une valeur VList dans tacinterp pour permettre de cabler desGravatar herbelin2006-09-22
| | | | | | | | Tactic Notation acceptant des listes en entrée avec application à la définition de revert dans Tactics.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
* incomplete and temporary fix for PR#1222: revert accepts up to 10 argsGravatar letouzey2006-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9156 85f007b7-540e-0410-9357-904b9bb8a0f7
* better scope/require managment (patch by Russel O'Connor)Gravatar letouzey2006-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indentation + typoGravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à une définition de inhabited plus dans les 'standard ↵Gravatar herbelin2006-08-28
| | | | | | mathématiques'; ajout preuve que tous les 'epsilon i P' sont égaux si P habité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9093 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Essai de remplacement de "ex P" par "exists x, P x" suite àGravatar herbelin2006-08-28
| | | | | | | | l'introduction d'unification de motifs à la Miller permettant une forme restreinte canonique d'unification du second ordre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9091 85f007b7-540e-0410-9357-904b9bb8a0f7
* JMeq maintenant applicable sur TypeGravatar herbelin2006-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9077 85f007b7-540e-0410-9357-904b9bb8a0f7
* comparison functions should be Defined not QedGravatar letouzey2006-08-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage sqtr_lem_1 (bug 1189)Gravatar notin2006-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵Gravatar herbelin2006-07-11
| | | | | | Rfun_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %F) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Argument Scope de list déplacé dans List.vGravatar herbelin2006-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2006-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques Hint inutilesGravatar herbelin2006-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9025 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ du manuel de référenceGravatar notin2006-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Zgcd_spec (compat.)Gravatar notin2006-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8990 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvel algorithme pour Zgcd (plus rapide) + un QcompareGravatar letouzey2006-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8989 85f007b7-540e-0410-9357-904b9bb8a0f7
* repetition d'hypotheses dans well_founded_induction_type_2Gravatar letouzey2006-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage des graphes de Function dans Type Gravatar jforest2006-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification déf de exists! pour éviter une éta-expansion et pouvoir ↵Gravatar herbelin2006-06-09
| | | | | | être filtré facilement par 'ex (unique ?P)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵Gravatar herbelin2006-06-09
| | | | | | DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 10:52:13 +0000