aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2004-11-18When a reference to a constructor is met its inductive type must be closed.sacerdot
This commit fixes the bug that prevented extraction of Lyon/CIRCUITS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6328 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-18Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6327 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Locate Moduleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6325 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17bug module with ... + vmbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6323 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6322 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17bug module M:=N avec vmbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6321 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Ajout 'Locate Module'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6320 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 08:58:54 +0000