aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2004-11-17Bug 'Locate Library lib' quand 'lib' est aussi un moduleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6318 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Déclaration de '..' comme mot-clé (résoud bug #856)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6316 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6315 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Suppression capture des variables par lieurs non liés dans Notation; ↵herbelin
simplification bound_binders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6314 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Suppression capture des variables par lieurs non liés dans Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6313 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Test lieurs dans Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6309 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17test-suite/output/Notations.outherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6308 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16Copy of the definition of prodT (already in the standard library) removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6306 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16dead (and obsolete) code (in comments) removedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6305 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-15bug coqmktop avec libcoqrun.a en bytecodebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6301 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-15Mise en conformité de Derive Inversion et Derive Dependent Inversion avec ↵herbelin
la doc (la forme 'with' du premier a été cassé dans la version 1.3 de leminv.ml (V7.0), tandis que la forme sans 'with' et le second étaient déjà cassés dans la V6.2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6300 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12*** empty log message ***gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6296 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-10Correction bug #868herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6292 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6289 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-09code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6288 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-08Prise en compte des notations récursives dans l'option 'format'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6286 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 22:40:04 +0000