aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-01-07Déplacement non-affichage des coercions dans termastherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@264 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Restructuration printer et parserherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@263 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Renommage command en constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@262 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-16erreurs de syntax :$filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@261 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-16bug : import -> export dans Requirefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@260 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15message erreur Schemeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@259 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Bug liftherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@258 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Les inductifs dans Scheme doivent être des ident d'inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@256 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14clarification du codefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@255 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@254 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14sauvegarde de la valeur de module_namefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@253 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14bug mk_clenv_from lorsque pas d argumentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@252 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14pretty-printers pour le debuggerfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@251 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13mise a jour de refiner.ml (reports de modifs de la V6.3)barras
bug possible dans lib.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@250 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13 - états fabriqués avec -silentfilliatr
- compilation theories avec -q - correction but de tclORELSE qui doit maintenant rattraper aussi TypeError et RefinerError git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@249 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13 - méthode load sur les Hintsfilliatr
- CAST pris en compte dans Astterm - Coercin.lookup_path_to_sort_from protégé par un try/with git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@248 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13chemin compile des fichiers Coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@247 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13petite erreur dans Commandfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@246 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13documentationfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@245 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13documentation interfacesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@244 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13fichiers prelude Coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@243 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13Poursuite intégration du Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@242 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12Ajout pp pattern et rawtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@241 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@240 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12modules et coqcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@239 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12modulesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12renommage (nom de module invalide)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@237 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11mise en place des outilsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@236 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11outils (manquent encore les deux filtres)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@235 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11Intégration initiale du Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@234 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11Quelques fonctions sur les locations des rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@233 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10bug: enregistrement de vartab au lieu de csttabfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@232 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10indications pour les developpeursfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@231 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10 - erreurs Pretypefilliatr
- Write / Restore State git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10debug resetfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10Suppression Rel de rawconstr et correction de bugs d'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@228 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10debug discharge et inductifsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@227 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09Ajout des messages d'erreurs de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@226 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09Bug affichage constructeurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@225 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09 - constantes avec recettesfilliatr
- discharge en deux temps, avec état remis comme au début de la section (mais c'est toujours buggé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09Discharge (encore bugge)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@223 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-08deplacement de Discharge dans toplevelfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-07link Dhyp et Autofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@221 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-07correction bug construct_referencefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@219 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@218 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-06Ajout option spéciale PPCherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@217 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-06Bug iterated_binderherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@216 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-06PPMultipleCase.v -> PPCases.v et MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@215 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 06:46:01 +0000