aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-12-08contrib/dpfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9418 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Pas d'escamotage des noms réservés si Set Printing All actibvéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9417 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Suite ajout option -output-contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9416 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 ↵filliatr
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Ajout d'une option -output-context qui affiche le contexte en CCI pur à laherbelin
sortie de session (nécessite option -batch) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9414 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Correction typo règle réduction du fix chapitre CCIherbelin
Maj mode emacs coqide dans faq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9412 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Subtac bug fix, add list take example.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9411 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-03MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9410 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-03Remplacement de la dépendance de G_vernac en G_constr (sourceherbelin
d'incohérences dans les dépendances en l'absence de g_constr.mli) par une dépendance en Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9409 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-01add a comment about Show Existentials and a question about case_eq jnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9408 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-29Fork of cases impl for subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9407 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-29correction du bug : VM value extraction error (PR#1290)bgregoir
Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9406 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 13:38:06 +0000