aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-12-28Correction petits bugs du check de la test-suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-28Remplacement de la définition de Pind et Prec par une définitionherbelin
suggérée par Conor McBride qui ne fait pas intervenir eq_rect et qui permet de montrer "facilement" (mais avec l'axiome K) les équations de réduction de Prec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9465 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-28Cleaning backtracking code, optimized "Backtrack n x y" when n iscourtieu
current state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-26Report correction bug #1289 dans trunk (r9435 pour branche v8.1)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9463 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-23Doc for Combined Scheme.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9462 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-23Addition of a "Combined Scheme" vernacular command for building the ↵msozeau
conjunction of mutual inductions principles. e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-22Default tactic for solving goals.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9460 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-22remplacement d'un test d'egalite par un test de convertibilite dans ↵jforest
injection/discriminate/inversion pour corriger des bugs en presence de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-21typo malencontreusefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9458 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-19Adaptation à Subversion 1.4notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9457 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-17reparation bug 1239letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9455 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
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
2006-12-15contrib/dp: tactique ergo (voir ergo.lri.fr)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9453 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-14Confusion sur le paramètre à donner à concrete_name lors du commit 9450herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9452 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-14Reimplemented equality generation for pattern matching at typing time. First ↵msozeau
version. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9451 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-13Alignement de la politique de renommage de rename_bound_var (utilisé pourherbelin
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
2006-12-13test condition de gardebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9449 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-13svn:ignoreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9448 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-13Dépliage du terme d'induction avant suppression quand celui-ci est unherbelin
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
2006-12-12Correction du bug #1273, deuxième version (avec des shémas d'elimination ↵notin
plus simples) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Correction du bug #1273 (problème avec les paramètres non récursivement ↵notin
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
2006-12-12Subtac: work on cases.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9444 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12nouvelle indentation des scriptsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9443 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12cosmetiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9442 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Variable print_instances pour déboguer les instances d'evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9441 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Dépendence inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9440 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12AllÃègement de syntxe suite à l'introduction de l'unif patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9439 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Bug nommage Zgt_trans_succherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9438 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Backtrack sur suppression des vars anonymes des contextes d'evars (echec ↵herbelin
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
2006-12-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9436 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Test bug #932herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9434 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Correction bug #1041 (double cause : non évitement des noms existants enherbelin
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
2006-12-11correction Open Local Scope (Ring)bgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9428 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-11Changement dans le kernel : bgregoir
- 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
2006-12-09Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9425 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-09Évitement des noms de constructeurs dans les motifs de filtrage de "match"herbelin
(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
2006-12-09git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 ↵filliatr
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08bug condition de gardebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9420 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08dpfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9419 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:13:07 +0000