aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Adaptation à Subversion 1.4Gravatar notin2006-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9457 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation bug 1239Gravatar letouzey2006-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
| | | | | | | | | maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
* contrib/dp: tactique ergo (voir ergo.lri.fr)Gravatar filliatr2006-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9453 85f007b7-540e-0410-9357-904b9bb8a0f7
* Confusion sur le paramètre à donner à concrete_name lors du commit 9450Gravatar herbelin2006-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reimplemented equality generation for pattern matching at typing time. First ↵Gravatar msozeau2006-12-14
| | | | | | version. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9451 85f007b7-540e-0410-9357-904b9bb8a0f7
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
| | | | | | | | résoudre la clause with de apply/elim) sur la politique de renommage de concrete_name git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9450 85f007b7-540e-0410-9357-904b9bb8a0f7
* test condition de gardeGravatar barras2006-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9449 85f007b7-540e-0410-9357-904b9bb8a0f7
* svn:ignoreGravatar herbelin2006-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépliage du terme d'induction avant suppression quand celui-ci est unGravatar herbelin2006-12-13
| | | | | | | | terme arbitraire, possiblement dépendant, qui a été transformé en let-in (cf success/destruct.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1273, deuxième version (avec des shémas d'elimination ↵Gravatar notin2006-12-12
| | | | | | plus simples) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1273 (problème avec les paramètres non récursivement ↵Gravatar notin2006-12-12
| | | | | | uniformes dans le cas de types mutuellement inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac: work on cases.Gravatar msozeau2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9444 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle indentation des scriptsGravatar barras2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9443 85f007b7-540e-0410-9357-904b9bb8a0f7
* cosmetiqueGravatar barras2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Variable print_instances pour déboguer les instances d'evarGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépendence inutileGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9440 85f007b7-540e-0410-9357-904b9bb8a0f7
* AllÃègement de syntxe suite à l'introduction de l'unif patternGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug nommage Zgt_trans_succGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur suppression des vars anonymes des contextes d'evars (echec ↵Gravatar herbelin2006-12-12
| | | | | | Case15.v et CasesDep.v pas anormal) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9437 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug #932Gravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
| | | | | | | | | | cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar + essai de ne pas faire dépendre les evars des variables anonymes afin de résoudre le bug #932 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction Open Local Scope (Ring)Gravatar bgregoir2006-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)Gravatar herbelin2006-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évitement des noms de constructeurs dans les motifs de filtrage de "match"Gravatar herbelin2006-12-09
| | | | | | | (un peu de doc de termops.mli au passage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9424 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 ↵Gravatar filliatr2006-12-09
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug condition de gardeGravatar barras2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9420 85f007b7-540e-0410-9357-904b9bb8a0f7
* dpGravatar filliatr2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9419 85f007b7-540e-0410-9357-904b9bb8a0f7
* contrib/dpGravatar filliatr2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'escamotage des noms réservés si Set Printing All actibvéGravatar herbelin2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite ajout option -output-contextGravatar herbelin2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9416 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 ↵Gravatar filliatr2006-12-08
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option -output-context qui affiche le contexte en CCI pur à laGravatar herbelin2006-12-08
| | | | | | | 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
* Correction typo règle réduction du fix chapitre CCIGravatar herbelin2006-12-08
| | | | | | | Maj mode emacs coqide dans faq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac bug fix, add list take example.Gravatar msozeau2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9411 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de la dépendance de G_vernac en G_constr (sourceGravatar herbelin2006-12-03
| | | | | | | | 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
* add a comment about Show Existentials and a question about case_eq Gravatar jnarboux2006-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9407 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction du bug : VM value extraction error (PR#1290)Gravatar bgregoir2006-11-29
| | | | | | | | Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9406 85f007b7-540e-0410-9357-904b9bb8a0f7
* The $(BEST) binaries symlinks depend on existence of target, not newness.Gravatar lmamane2006-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Functional graph merging deals with letins.Gravatar courtieu2006-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9404 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the graph merging parameter order.Gravatar courtieu2006-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9403 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the -emacs option which was always On.Gravatar courtieu2006-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing syntax and parameter order in functional graph merging.Gravatar courtieu2006-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mort découvert par MatthieuGravatar herbelin2006-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
| | | | | | | | 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
* un caractere blanc parasite dans svn:ignoreGravatar letouzey2006-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9396 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:38:57 +0000