aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-12-06Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6420 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Déplacement de la coercion vis à vis du but au niveau de Refine suite à ↵herbelin
changement de CastedOpenConstr en OpenConstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6419 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ↵herbelin
que de fonctions récursives même si l'une de ses fonctions n'a pas de meta); suppression gmm au passage suite commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6418 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Ajout bug #888herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Ajout bug #889herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6416 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06C'est trop compliqué de mettre à jour les types du metamap en passant sous ↵herbelin
les lieurs, plus simple de garder le type avec un cast (cf bug #889) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6415 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Inutile de réserver les notations à base de '{ }'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6410 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Commentaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6409 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵herbelin
tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06MAJ affichage nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6407 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Commentaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6405 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Bug (cf #892)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6403 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6402 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05MAJ changements ChoiceFactsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6401 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6400 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05Paramétrisation du domaine des axiomes de choix + ajout description = ↵herbelin
choice pour les propriétés décidables vers nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6399 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-04Bug 'set n in * |-'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6398 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-04Failed in 8.0pl1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6397 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-03Orthographe!herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6395 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-03Propagation du nom des hyps du prédicat de filtrage pour le message ↵herbelin
d'erreur elim_arity et réparation dans build_initial_predicate du bug mentionné dans success/Case8.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6394 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-03Was failing in 8.0pl1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6393 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-03Amélioration message d'erreur v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6391 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-01pp of nested fixpoints (dangling with/for)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6387 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-30Export pr_intro_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6385 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29UserError in reduce_to_*_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6382 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Complétion commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6381 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29*** empty log message ***gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6380 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Correction 1.138 appliquée à tort à la branche principale au lieu de ↵herbelin
V8-0bugfix; retour version 1.137 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6379 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Commit précédent erroné; retour version précédenteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6377 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-28Suppression bruit perlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6371 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-28Re-commit version nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6370 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-28MAJ vis à vis de extratacticsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6368 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-28Passage à la v8 pour test parserherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6367 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-28Pour ceux qui appelent Makefile avec des fichiers dans des sous-répertoiresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6365 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-27Complétion déclarations coqideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6362 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-27Indépendance vis à vis de Symbols (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6361 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26Correction bug #879herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6357 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26Réduire pour trouver l'arité d'une classeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6355 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26MAJ PCoFixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6352 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26backtrack of the last commit (it was my fault: the code is used bysacerdot
camlp4-generated code even if it is not found using grep) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6351 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26unused function in the interfacesacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6350 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22Bug commit 1.71herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6344 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6342 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22Correction bug Notation: il faut re-déclarer les règles de parsing des ↵herbelin
notations au moment de la déclaration d'interprétation car la règle de parsing peut être dans un autre fichier qui n'est pas importé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6340 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22Réparation incompatibilité de comportement introduite lors de mise en ↵herbelin
compatibilité avec Write State git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6339 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22compatibility with POWERPCgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-21Expansion Case dans injection et discriminate (cf bug #829)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6335 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-20'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marcheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6333 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-19Généralisation à Type de certaines propriétés des relationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6331 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6330 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 04:04:34 +0000