aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8687 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8686 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-06ouverture du bon scope (positive_scope) derriere le constructeur Npos de Nletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8685 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-06Enlevement de message d'erreur garbage.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8684 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses letouzey
avec des equivalences parametrees (genre forall n, P n <-> Q n) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8683 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05MAJ Licence FAQherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8682 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05on utilise explicitement Prop/iff pour certains morphismes pour eviter des ↵letouzey
warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8681 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05Suppression du test Proof with <tac>notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8680 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05ajout d'un rattrapage d'erreur pour "induction using".courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8679 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-04Bug index addendum à cause mauvaise utilisation asection dans Helm.texherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8678 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-02Correction bug 1119 (inversion marche a moitie dans Type)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8677 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-31Petite actualisation FAQherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8676 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-31Amendement impression evar pour affichage des Meta par 'info'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8675 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-30Réajout de eq_rec_eq oublié lors de la modularisation de Eqdepherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8674 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-29Ajout array_fold_map', list_fold_map' et list_remove_firstherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8672 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-29pour coqdocletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8671 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28Nommage explicite de certains "intro" pour préserver la compatibilitéherbelin
en préparation du passage à des inductifs à polymorphisme de sorte ("sigT R" va devenir de type le type de R, càd Set) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28- correction d'un bug dans coqdoc (multi_index)notin
- modif. de la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28Correction bug/typo dans splay_prod_assum et ajout decomp_sortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8668 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵letouzey
OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-27Correction d'un bug dans Coqdoc (indentation & mots clés)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8666 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-27- correction du bug #1055notin
- modification des propriétés sur trunk et trunk/test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8665 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-27appel Zenon sans preludefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8664 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-25 r8709@thot: notin | 2006-03-25 01:48:46 +0100notin
- Ajout de FSets dans la doc de stdlib - coqdoc copie la feuille de style dans le répertoire courant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8663 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-25 r8708@thot: notin | 2006-03-24 18:55:01 +0100notin
Correction d'un bug sur la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8662 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-25 r8686@thot: notin | 2006-03-20 19:29:09 +0100notin
Correction d'un bug dans Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8661 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-24utilisation de la VM pour la normalisation finale de romegaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8660 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-24Patch envoy\'e par Benjamin Gregoire, permettant de corrigerletouzey
un probleme avec normalise_vm_in_concl git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8659 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-23on ignore TAGS au niveau svnletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8658 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-23correctifs de bug pour romega: letouzey
1) dans refl_omega, on donnait a OmegaSolver un generateur de numero d'equations new_eq_id qui pouvait clasher avec les numeros d'equations initiaux créés avec new_omega_id. => on sépare en deux compteurs, un pour les equations omegas, l'autre pour les variables omegas. On en profite pour reinitialiser ces compteurs à chaque session romega, histoire que romega devienne reproductible. 2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti à un endroit. ATTENTION: ceci peut changer le comportement d'omega. Surveiller le resultat du prochain bench nocturne. 3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication dans une hypothese lors du recalcul final. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-23Correction d'un bug sur 'make doc' et modification des propriétés dans doc/notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8656 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Subtac fixes, single fixpoint definitions are working again. Added a toggle ↵msozeau
on the pretyping module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where constructors have arguments). Does not change current behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default ↵msozeau
uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22- Correction bug calcul mind_consnrealargs, introduit à la révisionherbelin
7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deherbelin
la compilation de fichiers comme hipattern.ml (renommé en hipattern.ml4) - Extension de eqdecide.ml4 pour qu'il gère les buts sans quantificateurs, basés soient sur sumbool soit sur or, et à symétrie près de la disjunction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-21+ destruct now works as induction on multiple arguments : jforest
destruct x y z using scheme + replace c1 with c2 <in hyp> has now a new optional argument <as tac> replace c1 with c2 by tac tries to prove c2 = c1 with tac + I've also factorize the code correspoing to replace in extractactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-21git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8650 ↵letouzey
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-20Adding "New Functional Scheme" jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8649 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-18Documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8648 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-18MAJ documentation en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8647 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-18Bug BYTEFLAGS pour compilation bin/parserherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8646 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-18Documentation mutual_inductive_bodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8645 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-18Bug calcul consnrealargs + bug calcul occurrences non positives + modifs ↵herbelin
cosmétiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8644 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17MAJ debugging (et arrêt support version française)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8643 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17Modification des propriétés (svn:executable)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17ajout d'un debut de proprietes pour les FSetWeakletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-16deux tags $ mal formesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8640 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-16propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble ↵letouzey
des fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-16afin que svn ignore les liens symb coqide et coqtopletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8638 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:09:52 +0000