aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04resolution du pb d'efficacite du a Sign.add_named_declbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-03renommage de l'exception locale Aritybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2606 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-29*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2576 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-28petite erreur dans le typage des let-inbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2573 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-22code redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2565 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-12open Univ inutilecourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2524 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22suppression de pop_namedbarras
meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-11substitution et pattern modulo letbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07erreur mineure dans le test des inductifs imbriquesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2461 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07petit nettoyage de kernel/inductivebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-05evaluable_constant retournait vrai pour les constantes opaques, ce qui faisaitbarras
boucler la condition de garde git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2454 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31changement generation de schema d'elimination, False_rec est primitif, ↵mohring
Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-30cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2445 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-30Reparation erreur de syntaxemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2443 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-29modification de la definition des def inductives unitaires et autorisation ↵mohring
d'elimination sur la sorte Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2442 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-29condition de positivite moins stricte vis-a-vis des parametres (cf bug de ↵barras
Eduardo) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2441 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-24Cas LetIn superflu dans check_construct car normalisation préalableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2428 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-16correction de bug avec les mutuels imbriques a plusieurs niveauxbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2401 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-20Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2353 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Bug de de Bruijn pour le LetInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2348 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Le cas LetIn avait été oublié dans case_branches_specifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2324 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19reparation de make doc (ocamlweb & _)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2321 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10- condition de garde (suite)barras
- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-04bug fix de la condition de gardebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2264 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30desobfuscation du code de la verif de la condition de gardebarras
reparation bug de la tactique CutRewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2261 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-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-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-20Ajout isEvarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2220 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-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-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-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-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-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09MAJ pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2177 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Rétablissement de la persistance des Cast; typage des LetIn sans recours à ↵herbelin
Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:20:05 +0000