aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Collapse)AuthorAge
* Préférence donnée aux constantes qui ne sont pas des projectionsGravatar herbelin2008-06-29
| | | | | | | | | | | | canoniques lors d'une unification constante/constante s'apprêtant à déplier l'une des deux constantes (suggestion des utilisateurs de structures canoniques), ceci afin de préserver des possibilités ultérieures de résolution d'evars par équipement en structure canonique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11187 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptées. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiées (au lieu de traiter seulement les buts t1<>t2). --This line, and those below, will be ignored-- M doc/refman/RefMan-tac.tex M CHANGES M pretyping/evd.ml M pretyping/termops.ml M pretyping/termops.mli M pretyping/clenv.ml M tactics/extratactics.ml4 M tactics/inv.ml M tactics/equality.ml M tactics/tactics.mli M tactics/equality.mli M tactics/tacticals.ml M tactics/eqdecide.ml4 M tactics/tacinterp.ml M tactics/tactics.ml M tactics/extratactics.mli M toplevel/auto_ind_decl.ml M contrib/funind/invfun.ml M test-suite/success/Discriminate.v M test-suite/success/Injection.v M proofs/clenvtac.mli M proofs/clenvtac.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
| | | | | | | | (résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.Gravatar herbelin2008-06-10
| | | | | | | - Test match dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11095 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
| | | | | | | | | | | | | | | | | - Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
| | | | | | | | generalized hypotheses. Also move part of the tactic to ML and improve the generated proof term in case of non-dependent induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
| | | | | | | camlp4. Petit nettoyage en passant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait d'un test commité par erreur en 10947Gravatar herbelin2008-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10949 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration de micromega ("omicron" pour fourier et sa variante sur Z,Gravatar herbelin2008-05-19
| | | | | | | | | | | "micromega" et "sos" pour les problèmes non linéaires sous-traités à csdp); mise en place d'un cache pour pouvoir rejouer les preuves sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra affiner cela). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes:Gravatar msozeau2008-05-15
| | | | | | | | | | | | - Fix a typo in lowercase_utf8 - Fix generation of signatures in subtac_cases not working for dependent inductive types with dependent indices. - Fix coercion of inductive types generating ill-typed terms. - Fix test script using new syntax for Instances. - Move simpl_existTs to Program.Equality and use it in simpl_depind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Résolution des problèmes ambigus d'inférence du type de retour desGravatar herbelin2008-05-14
| | | | | | | | | problèmes de filtrage au nivau de consider_remaining_unif_problems (résoud en particulier le "bug" #1851). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10927 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | du filtrage. Cela permet de détecter les cas impossibles et de simuler les contraintes d'inversion exprimables sous la forme d'un assignement des arguments du constructeurs (cf le cas de Vtail dans Bvector.v). Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi) avec vi composé uniquement de constructeurs, et que le résultat final est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on construit le prédicat Q:=fun x1 .. xn y => match x1 .. xn y with | v1(z) .. vn(z) t => P(z) | _ .. _ _ => ?evar-speciale-cas-impossible end qui vérifiera bien que Q u1 .. un = P(w1,..,wp). En raison de limitations de l'unification (on aurait besoin d'eta conversion pour résoudre des problèmes du genre "terme rigide == match x with _ => ?evar end", et besoin d'instanciation par constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"), je n'ai pas réussi à traiter le cas général. Aussi, on adopte une stratégie pragmatique consistant à tester plusieurs prédicats possibles : - si un type final est donné, on essaie d'abord l'algorithme de Matthieu et sinon le nouvel algorithme (permet par exemple de traiter certains cas d'élimination dépendante de Bvector.v), - s'il n'y a pas de type final, on essaie d'abord le nouvel algo et sinon, on essaie avec un prédicat sans dépendance (permet de traiter des cas compliqués comme celui de par cas sur I' dans le fichier Case13.v de la test-suite). Dans la pratique, il y a beaucoup de changement dans le code de compile_case. - Par exemple, la compilation est maintenant toujours appelé avec un prédicat (là où l'on pouvait avoir None, on a maintenant toujours au moins une evar). - En revanche, le membre droit des clauses est maintenant optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une branche impossible au moment du calcul du prédicat de retour. - Aussi, on renonce aux PrLetIn et PrProd dans l'expression du predicat de retour mais il faut savoir que c'est maintenant la liste des tomatchs qui spécifie le contexte exact dans lequel le prédicat de retour est bien typé. - Et d'autres... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
| | | | | | | | | | | particulier, TacCall(_,f,[]) est utilisé pour une référence à une variable ltac ou une tactique et Reference(f) est utilisé pour une référence à une variable ltac ou un constr (en passant, standardisation de l'utilisation de constr: ou ltac: à setoid_ring). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
| | | | | | | | | | | bug "no level labelled 8" (camlp5 ne sait pas annuler un extend lorsque le niveau initial existe mais est vide : l'appel à delete efface le niveau au lieu d'annuler l'effet de extend et de revenir à un niveau existant vide). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
| | | | | | | | | | - pour le "try", la nouvelle erreur CannotFindWellTypedAbstraction doit être catchable - pour accomoder Type -1 dans le discharge, il faut un refresh_universes strict - bugs dans les fichiers de test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10861 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
| | | | | | | | | | | | - Un patch pour le bug de non vérification du typage de Stéphane L. - Changement du fameux message "cannot solve a second-order matching problem" en espérant, à défaut de savoir résoudre plus souvent le problème, que le message est plus explicite. - Divers changements cosmétiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
| | | | | | | | | | | des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | de l'argument donné contient des métavariables (souhait #1408). Beaucoup d'infrastructure autour des constantes pour cela mais qu'on devrait pouvoir récupérer pour analyser plus finement le comportement des constantes en général : 1- Pour insérer les coercions, on utilise une transformation (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml. 2- Pour la compatibilité, on s'interdit d'insérer une coercion entre classes flexibles parce que sinon l'insertion de coercion peut prendre précédence sur la résolution des evars ce qui peut changer les comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN). 3- Pour se souvenir rapidement de la nature flexible ou rigide du symbole de tête d'une constante vis à vis de l'évaluation, on met en place une table associant à chaque constante sa constante de tête (heads.ml) 4- Comme la table des constantes de tête a besoin de connaître l'opacité des variables de section, la partie tables de declare.ml va dans un nouveau decls.ml. Au passage, simplification de coercion.ml, correction de petits bugs (l'interface de Gset.fold n'était pas assez générale; specialize cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml]; whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml]) et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml, classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
| | | | | | | | | | | | | | | | - Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix setoid tests, use red for a Setoid_Theory lemma, and ParametricGravatar msozeau2008-04-14
| | | | | | | Relation for function spaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
| | | | | | | | | | | | | | | | | | | | | | - vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction problème de compil (blast.ml)Gravatar herbelin2008-04-04
| | | | | | | | Correction bugs commentaires pour coqdoc (ChoiceFacts.v) Test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chgts mineurs:Gravatar herbelin2008-04-03
| | | | | | | | | | - correction commit incorrect d'une modif de test-suite/success/apply.v - réorganisation dev/ - renommage Print Modules en Print Libraries - $Id:$ dans g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
| | | | | | | | | | | alleviate some problems with delta. Better precedence in lambda notation. Temporarily deactivate notations for relation conjunction, equivalence and so on, while we search for a better syntax and maybe a generalization (fixes bug #1820). Better destruct_call in Program.Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
| | | | | | | | pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite files, change conflicting notation "->rel" and the othersGravatar msozeau2008-03-29
| | | | | | | | | | to "-R>" and the like. Split more precisely in inference of case predicate between the new code which currently works only for matched variables and the old one which works better on variables appearing in matched terms types (the two could also be merged). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | Add definitions of relational algebra in Classes/RelationClasses including equivalence, inclusion, conjunction and disjunction. Add PartialOrder class and show that we have a partial order on relations. Change SubRelation to subrelation for consistency with the standard library. The caracterization of PartialOrder is a bit original: we require an equivalence and a preorder so that the equivalence relation is equivalent to the conjunction of the order relation and its inverse. We can derive antisymmetry and appropriate morphism instances from this. Also add a fully general heterogeneous definition of respectful from which we can build the non-dependent respectful combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | | [in I] := t [return pred] in b", just as SSReflect does with let:. Change implementation: no longer a separate AST node, just add a case_style annotation on Cases to indicate it (if ML was dependently typed we could ensure that LetPatternStyle Cases have only one term to be matched and one branch, alas...). This factors out most code and we lose no functionality (win ! win !). Add LetPat.v test suite. - Slight improvement of inference of return clauses for dependent pattern matching. If matching a variable of non-dependent type under a tycon that mentions it while giving no return clause, the dependency will be automatically infered. Examples at the end of DepPat. Should get rid of most explicit returns under tycons. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses petites modifs dans la test-suite:Gravatar notin2008-03-26
| | | | | | | | | | | | | | | | | | | | | | | | test-suite/output/ZSyntax.out typo test-suite/bugs/closed/shouldsucceed/1776.v bug closed test-suite/success/extraction.v test-suite/success/extraction.v test-suite/bugs/closed/shouldsucceed/846.v backtrack sur le commit 10639 test-suite/bugs/closed/shouldsucceed/1322.v: petites modifications suite aux changement de setoid_replace test-suite/bugs/closed/shouldsucceed/1414.v: petites modifications suite aux changement dans Program git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc: Add test for bug 1704, now closed. Add usual syntax for lists inGravatar msozeau2008-03-16
| | | | | | | | Program.Syntax along with stronger implicits. Update dependent induction test file using unicode syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot the test file.Gravatar msozeau2008-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur le test censé discriminer entre une erreur d'evar nonGravatar herbelin2008-03-15
| | | | | | | | | | résolue et une anomalie. Il ne marche pas. La question de trouver la bonne manière de tester qu'un exemple renvoie une erreur (non rattrapable par tactique) et une anomalie reste ouverte. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
| | | | | | | | | - Correction bug des filtres dans define_evar_as_abstraction - Nettoyage, documentation et réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10650 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of Add Relation as a DefaultRelation instanceGravatar msozeau2008-03-08
| | | | | | | | declaration. Really fix bug#1704, correct order of condition subgoals even in setoid_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
| | | | | | | | | | | | | | | | | | implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * "f_equal" is now a tactic in ML (placed alongside congruence since it uses it). Normally, it should be completely compatible with the former Ltac version, except that it doesn't suffer anymore from the "up to 5 args" earlier limitation. * "revert" also becomes an ML tactic. This doesn't bring any real improvement, just some more uniformity with clear and generalize. * The experimental "narrow" tactic is removed from Tactics.v, and replaced by an evolution of the old & undocumented "specialize" ML tactic: - when specialize is called on an hyp H, the specialization is now done in place on H. For instance "specialize (H t u v)" removes the three leading forall of H and intantiates them by t u and v. - otherwise specialize still works as before (i.e. as a kind of generalize). See the RefMan and test-suite/accept/specialize.v for more infos. Btw, specialize can still accept an optional number for specifying how many premises to instantiate. This number should normally be useless now (some autodetection mecanism added). Hence this feature is left undocumented. For the happy few still using specialize in the old manner, beware of the slight incompatibities... * finally, "contradict" is left as Ltac in Tactics.v, but it has now a better shape (accepts unfolded nots and/or things in Type), and also some documentation in the RefMan git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10637 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nGravatar herbelin2008-03-06
| | | | | | | | | dans certains cas. Branchement au passage de w_unify vers evar_conv et solve_simple_eqn en cas d'équations entre Evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'une typo restant du commit 10557 et cause d'échec de contribsGravatar herbelin2008-03-05
| | | | | | | | telles que Godel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10622 85f007b7-540e-0410-9357-904b9bb8a0f7
* congruence now knows about _ -> _Gravatar corbinea2008-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10579 85f007b7-540e-0410-9357-904b9bb8a0f7
* added products and sorts as possible heads for canonical structuresGravatar corbinea2008-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added default canonical structures (see example in test-suite)Gravatar corbinea2008-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug de clearGravatar notin2008-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10552 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug à l'interprétation de "change" (on exigeait queGravatar herbelin2008-02-06
| | | | | | | | l'argument soit un type même lorsque c'était un terme qu'on convertissait). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
| | | | | | | | | | | | | | | | | | | | | | | | maintenant écrire des fonctions récursives qui n'ont pas l'apparence d'être fonctionnelle. La sémantique reste toutefois différente. Par exemple, dans Ltac is := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. l'évaluation de i est paresseuse, alors que dans une version non récursive Ltac is := let i := match goal with |- ?A -> ?B => intro | _ => idtac end in i. l'évaluation de i est forte (et échoue sur le "match" qui n'est pas autorisé à retourner une tactique). (note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debug implementation of dependent induction/dependent destruction and ↵Gravatar msozeau2008-01-31
| | | | | | document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un test pour le mode déclaratif + test pour le bug #1776Gravatar notin2008-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10466 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better resolution of implicit parameters in typeclass binders, add ↵Gravatar msozeau2008-01-02
| | | | | | extensionality tactic to apply the axiom properly and fix test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Complément aux commits 10124 et 10125 sur l'inférence de type (correction Gravatar herbelin2007-09-26
| | | | | | | | | de plusieurs bugs d'indice, de List.rev, d'oubli d'application de whd_evar + code plus concis pour l'argument optionnel "filter"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)Gravatar herbelin2007-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10125 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 05:38:48 +0000