aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-11-30Integration de nouveaux lemmesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2253 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2252 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30Intégration de nouveaux lemmes.desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2251 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30Ajout d'un "\" pour proteger un autre "\" et ainsi etre compatible avecclrenard
ocaml 3.03 malgre un bug de lexing dans camlp4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2250 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29Mise a jour des dependancesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2249 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2248 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29reparation de Locatebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-22 08:11:12 +0000