aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* La mise en forme normale du prédicat d'élimination était un peu trop ↵Gravatar herbelin2001-11-22
| | | | | | violente pour la compatibilité de la synthèse des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration message CasesGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques autres petits problèmes résolus...Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2239 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2238 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration messages d'erreur arité incorrecte (notamment record)Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Possibilité d'appeler check avec l'option -byteGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification de la propagation du prédicat, bugs, et messages d'erreursGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2234 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation de mes actions recentes sur les theories (PL)Gravatar letouzey2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2233 85f007b7-540e-0410-9357-904b9bb8a0f7
* remise au gout du jour du repertoire theories/Sorting de la V6.3Gravatar letouzey2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2232 85f007b7-540e-0410-9357-904b9bb8a0f7
* remise au gout du jour du repertoire theories/Sorting de la V6.3Gravatar letouzey2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
* La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solution partielle au problème des alias dépendants pour les rendre ↵Gravatar herbelin2001-11-21
| | | | | | compatibles avec l'utilisation de la contrainte de type comme guide de la synthèse du prédicat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2229 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des '?' aussi dans le type des définitionsGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2228 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli des contraintes d'univers lors de la suppression des cast dans un ↵Gravatar herbelin2001-11-21
| | | | | | commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make sure that NatRing won't loop forever.Gravatar bertot2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un bug dans le scriptGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sur l'exahustivité du filtrageGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sur la cumulativité dans les tactiquesGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux exemplesGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des coercions pour typer les branches lorsqu'il y a une ↵Gravatar herbelin2001-11-21
| | | | | | contrainte de type sur le résultat du Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout isEvarGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2220 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout make_arity_signatureGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2219 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout mkArityGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2218 85f007b7-540e-0410-9357-904b9bb8a0f7
* hack temporaire concernant les remarks/modulesGravatar letouzey2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2217 85f007b7-540e-0410-9357-904b9bb8a0f7
* iota généraliséGravatar letouzey2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2216 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2215 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug contrainte de valeur trop restrictive sur le typage du type ↵Gravatar herbelin2001-11-20
| | | | | | du Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2214 85f007b7-540e-0410-9357-904b9bb8a0f7
* types vs constrGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2213 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug mauvaise instanceGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2212 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
* types vs constrGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cosmétique avant toutGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2209 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des Cast externes dans les définitionsGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2208 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout quelques fonctions; code mortGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2206 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug nommage des fonctions définies par récursion mutuelleGravatar herbelin2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2205 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'une méthode directe pour indiquer le type des déclarations ↵Gravatar herbelin2001-11-19
| | | | | | à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-installation de l'affichage des globaux par des noms courtsGravatar herbelin2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2202 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage qualid_of_global en shortest_qualid_of_globalGravatar herbelin2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2201 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-installation de l'affichage des globaux par des noms courtsGravatar herbelin2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2200 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remise en place du Cast pour CorrectnessGravatar herbelin2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2199 85f007b7-540e-0410-9357-904b9bb8a0f7
* User Casts are for helping pretyping, experimentally not to be keptGravatar herbelin2001-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2198 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2197 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2196 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un fichier Max dans Arith, et enrichissement du Min.Gravatar letouzey2001-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des fonctions tail-recursives tail_plus et tail_mult.Gravatar letouzey2001-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une liste plus precise des .v a prendre en compte pour les dependances, a ↵Gravatar herbelin2001-11-14
| | | | | | l'exclusion notamment des .v de la suite de tests git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2193 85f007b7-540e-0410-9357-904b9bb8a0f7
* oubli: changement de nil en nilTGravatar mayero2001-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2192 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 16:31:22 +0000