aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-11-27The $(BEST) binaries symlinks depend on existence of target, not newness.lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9405 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Functional graph merging deals with letins.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9404 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Fixed the graph merging parameter order.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9403 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Fixed the -emacs option which was always On.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9402 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-23Fixing syntax and parameter order in functional graph merging.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9401 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-22Code mort découvert par Matthieuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9399 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-21Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deherbelin
chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-21un caractere blanc parasite dans svn:ignoreletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9396 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Changing merging functional scheme syntax.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9395 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Correction boucle du parseur en cas de caractÃère non unicodeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9394 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Suppression du type 'tac dans les abstract_argument_type: devenu inutile herbelin
suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des wit_tactic en types créés dynamiquement (révisions 8917 et 8926). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9393 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-19Dépendance inutile en Tacexpr, de proofs, qui se compile en principe aprèsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9392 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-19mult_sym, plus_sym -> mult_comm, plus_commherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9391 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-19MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9390 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
degrés de liberté concernant les instances de méta (cumulativité et possibilité d'éta-expansion) de telle sorte que la fusion d'équations se fasse modulo ces degrés de liberté. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9389 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-18Code mort (duplication de code dans reductionops.ml)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9388 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-17The emacs-U option now does not output *any* char above 250.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9384 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16Small fix in functional graph merging.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9383 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16suppression de code mort (avec bug de nom)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9382 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16pb avec r9379 + modifs dans ringbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9381 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16Work on dep types pattern matchingmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9380 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16suite de r9362: reconnaissance de qqs injections entre nat, N et Zbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9379 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16Adaptation à FreeBSDnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9378 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-15Some usability enhancements.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9376 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Better solve using tactics impl.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9374 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Correction de la seconde partie du bug #1278jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9373 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Correction de la premiere partie du #1278 (but non referme en cas d'echec)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9372 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9371 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Encore des _sym au lieu de _commherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9370 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Correction typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9369 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-11Fichiers obsolètesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9367 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-11Typo + ajout Qcanon.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9366 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Ajout de dépliage de l'énoncé, si besoin est, dans apply inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9363 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10generalisation de ring pour faire Ring_nfbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9361 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Work on mutual defs, various bug fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9360 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Correction d'un bug refineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9359 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Work on pattern inequalities for pattern matching branches.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9358 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-09Support for mutual defs in obligation handling.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9357 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-07Changement des modifeurs par défaut dans CoqIDE (problème de ↵notin
compatibilité entre architecture) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9349 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-07git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9348 ↵filliatr
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-06Changement du magic numbernotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9346 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-05fixes PR#1269 about function: there is no reason well founded induction isbertot
limited to only Set and not any type in Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9340 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-03Suppression source de complexité polynomiale introduite par le polymorphismeherbelin
dans les définitions alors même que ce polymorphisme est débranché git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9336 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-03bug test complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9335 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-02gestion speciale du niveau 5 des ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-02Add doc on obligation solving commands.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9332 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-01Quick hack to solve to complexity issue in function mark_occurherbelin
(but should probably not work in presence of morphisms to Leibniz's equality). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9331 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-01Ajout test setoid_rewrite (cf bug #1176); anglicisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9330 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Debug obligation handling codemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9329 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Retour sur la modification apportée en r9289, et nouvelle correction du bug ↵notin
#1259 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9328 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:03:43 +0000