aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2245 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-27mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2244 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-23Retablissement de la commande Existential que j'avais supprime par erreur.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2243 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2242 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-22La mise en forme normale du prédicat d'élimination était un peu trop ↵herbelin
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
2001-11-21Amélioration message Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2240 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Quelques autres petits problèmes résolus...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2239 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2238 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2237 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Amélioration messages d'erreur arité incorrecte (notamment record)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2236 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Possibilité d'appeler check avec l'option -byteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2235 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Simplification de la propagation du prédicat, bugs, et messages d'erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2234 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21documentation de mes actions recentes sur les theories (PL)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2233 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21remise au gout du jour du repertoire theories/Sorting de la V6.3letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2232 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21remise au gout du jour du repertoire theories/Sorting de la V6.3letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2230 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Solution partielle au problème des alias dépendants pour les rendre ↵herbelin
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
2001-11-21Prise en compte des '?' aussi dans le type des définitionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2228 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Oubli des contraintes d'univers lors de la suppression des cast dans un ↵herbelin
commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2227 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Make sure that NatRing won't loop forever.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2226 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Un bug dans le scriptherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2225 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Sur l'exahustivité du filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2224 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Sur la cumulativité dans les tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2223 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Nouveaux exemplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2222 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Prise en compte des coercions pour typer les branches lorsqu'il y a une ↵herbelin
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
2001-11-20Ajout isEvarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2220 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout make_arity_signatureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2219 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout mkArityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2218 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20hack temporaire concernant les remarks/modulesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2217 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20iota généraliséletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2216 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2215 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Correction bug contrainte de valeur trop restrictive sur le typage du type ↵herbelin
du Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2214 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20types vs constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2213 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Bug mauvaise instanceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2212 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20types vs constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Cosmétique avant toutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2209 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Suppression des Cast externes dans les définitionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2208 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2207 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout quelques fonctions; code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2206 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Bug nommage des fonctions définies par récursion mutuelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2205 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Mise en place d'une méthode directe pour indiquer le type des déclarations ↵herbelin
à 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
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2202 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Renommage qualid_of_global en shortest_qualid_of_globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2201 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2200 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Remise en place du Cast pour Correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2199 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-17User Casts are for helping pretyping, experimentally not to be keptherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2198 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2197 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2196 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-13 13:32:05 +0000