aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
| | | | | | | instantiation of evars in tacticals (cf r9985, r10294). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Util.option_compare devient Option.Misc.Compare et change un peu de type Gravatar aspiwack2007-12-07
| | | | | | | | | | ( ('a -> 'b -> bool) -> 'a option -> 'b option -> bool devient la même chose mais avec 'a='b ) et de contenu pour avoir une sémantique plus claire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enlevé les trucs commités au mauvais endroitGravatar aspiwack2007-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques structures de donnée plus les modules principaux (et Gravatar aspiwack2007-10-23
| | | | | | | | parfaitement en cours) de la nouvelle machinerie de preuves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10251 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
| | | | | | | | Ajout de l'option with à (e)destruct et (e)induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
| | | | | | | | | | | Printing Universes est active. Ajout de l'option "using" à la tactique non documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto decomp" avec des principes élémentaires tels que le dépliage de "iff". Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ----------------------------------------------- - Les fonctions evar_define et real_clean font un travail plus fin : - S'il y a plusieurs manières d'inverser l'instance d'une evar, on retarde le choix au lieu de faire un choix arbitraire. - Si l'instance contient une evar et que cette evar n'est pas inversible, on essaie aussi d'inverser ou de restreindre (un sous-terme) de l'evar qui était initialement à instancier. - Incidemment, real_clean est renommé en invert_instance, un nom qui reflète mieux la diversité du travail fait par ce fameux real_clean. - La fonction solve_refl garde les problèmes qui contiennent encore de l'information. - Changements secondaires : - Délégation de la gestion des variables modifiées et des problèmes à reconsidérer (get_conv_pbs) à Evd (qui s'en charge par effet de bord au moment du define) (incidemment get_conv_pbs devient extract_conv_pbs) - Essai d'un mécanisme différent de restriction des evars : pour éviter des contextes mal formés (comme do_restrict pouvait a priori le faire), on utilise maintenant un contexte bien formé doublé d'un filtre signalant les instances interdites. C'est a priori plus souple (par ex : si une variable du contexte a un type dépendant d'une evar, on peut attendre de connaître cette evar avec de déterminer si cette variable du contexte, qui peut-être dépend via cette evar d'une autre variable interdite, doit être finalement interdite ou pas) - Nettoyages divers. - Ce que evarutil ne fait toujours pas : - Utiliser l'inversion et/ou l'unification d'ordre supérieur (par exemple pour résoudre "?ev[S n]=n"); en particulier, la notion d'inversion unique ne prend pas en compte l'unification d'ordre supérieur et peut donc faire des choix irréversibles vis à vis de l'unif d'ordre supérieur. - Utiliser (systématiquement -- et précautionneusement) les types des solutions trouvées pour résoudre davantage de problèmes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
| | | | | | | evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
| | | | | | | | Cleaner code: the guardedness bug is now corrected. Added "trivial" to the automation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12
| | | | | | | | | * explicitation of some types * tags for grammar entries git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
| | | | | | | | | | | | | | | | | | | | | | rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
| | | | | | | | rename A into B, C into D, E into F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
| | | | | | | | | (cas d'un terme sans Rel libre), introduction au passage d'un nouveau type d'evar EvarGoal pour raffinement du message d'erreur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | de résoudre des buts comme celui-ci : Record nat_retract : Type := {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}. Goal nat_retract. exists (fun x => x) (fun x => x). - Nouvelle tentative d'utilisation des types des metas/evars pour inférer de nouvelles instances de metas/evars; permet par exemple d'utiliser f_equal sans option with, mais aussi, avec la modif précédente, de résoudre des buts tels que Goal exists f:bool->Prop, f true = True. exists (fun x => True). [Les expériences passées avaient montré qu'en prenant en compte les types dans l'unification, on peut unifier trop tôt une evars à une mauvaise sorte; à défaut de mécanisme de prise en compte des problème d'unification avec sous-typage, on s'est interdit ici d'unifier des types qui sont des arités.] - Tout les constr de tactic_expr deviennent des open_constr (même si seul with_bindings les accepte au final... c'est pas l'idéal). - Renommage env -> evd et templenv -> env dans clausenv. - Renommage closed_generic_argument -> typed_generic_argument. - Renommage closed_abstract_argument_type -> typed_abstract_argument_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1519Gravatar herbelin2007-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
| | | | | | | | | par sa notation (p.ex. pour unfold ou pour lazy delta). Ex: Goal 3+4 = 7. unfold "+". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
| | | | | | | | | Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et ↵Gravatar notin2007-04-26
| | | | | | uniformisation des messages d'erreur wrt instantiate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9798 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin des conclusions multiplesGravatar corbinea2007-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
| | | | | | | | | | | | | | | | | | | | | | | fix/cofix avec réutilisation du nom de la constante dans les appels récursifs), avec notamment uniformisation des comportements et des noms de fonctions de réduction. En particulier, on a les changements sémantiques suivants : - léger changement de simpl: si appliqué à un fix explicite, il sait réduire l'argument en un constructeur comme si le fix était caché derrière une constante (cf exemple dans test-suite/output/reduction.v); - léger changement de hnf: si appliqué à un match ou un fix explicite et que l'argument de ce match ou de ce fix nécessite un calcul impliquant des constantes récursives, il sait conserver les noms (à la manière de simpl) comme il sait déjà le faire si ce match ou ce fix était caché derrière une constante (cf exemple dans test-suite/output/reduction.v); - changement similaire de one_step_reduce utilisé dans reduce_to_*_ref (difficile d'imaginer les effets mais sans doute très peu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension to the general sequence operator (tactical). Now in addition to ↵Gravatar emakarov2007-04-02
| | | | | | | | | | | the form expr_0 ; [ expr_1 | ... | expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0. The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command expr_0; [expr_1 | ... | expr_i .. | ... | expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de révision 9583 de la v8.1 dans le trunkGravatar notin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de code mortGravatar notin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
| | | | | | | | la gestion des erreurs dans clear_hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9560 85f007b7-540e-0410-9357-904b9bb8a0f7
* "suffices" implemented + syntax cleanupGravatar corbinea2007-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
* decl mode: anonymous factsGravatar corbinea2007-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1315:Gravatar notin2007-01-22
| | | | | | | | | | | | | | | | | | - ajouts des opérations clear_evar_hyps_in_evar, clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui permettent de supprimer des hypothèses dans le contexte des evars, en créant une nouvelle evar avec un contexte restreint; - adaptation de clear_hyps dans Logic pour qu'elle mette à jour le contexte des evars; - adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié; - déplacement de la tactique Change_evars dans prim_rule. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | comportement pré-inductifs polymorphes vis à vis du test d'inclusion des hypothèses de section (i.e. test dans le noyau mais pas dans typing.ml qui est le typeur utilisé généralement par les tactiques). En effet, les variables de section sont vues par les tactiques comme des variables locales qui sont modifiables (p.ex. par conversion). Mais le changement de la signature des variables de section fait échouer le typage noyau (qui exige une égalité syntaxique des types de ces variables) pour les demandes de typage en provenance des tactiques. Quelle est la bonne solution ? - Faut-il comparer les variables de section modulo réduction dans le noyau ? - Faut-il continuer à utiliser un typeur qui ne teste pas les hyps de section pour les tactiques, comme c'était le cas avant les inductifs polymorphes (c'est la solution pragmatique adoptée pour résoudre #1325) - Faut-il éviter la confusion entre variables de section et variables de but ? Incidemment, branchement de Tacmach.hnf_type_of sur Retyping, ce qui, outre des calculs de typage allégés pour les tactiques, évite aussi de tomber sur le comportement du bug #1325. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9510 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
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
| | | | | | | | 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
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
| | | | | | | | | | | | (trop de problèmes à régler, comme par exemple des types identiques qui se retrouvent dans des sortes disjointes, résultant en davantage d'équations (eq Type(i) a b) et (eq Type(j) a b) avec i syntaxiquement distinct de j, que Coq ne sait en général pas traiter -- i.e. ne sait pas forcer i==j (cf contrib CatsInZF: échec du test "dependent" dans "rewrite"); autre problème: le ralentissement du prouveur (logic.ml)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
| | | | | | | | | Amélioration affichage des univers. Réparation de petits oublis du premier commit. Essai d'une nouvelle stratégie : si le type d'une constante est mentionné explicitement, la constante est monomorphe dans Type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
| | | | | | | | | | (suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de la primitive ltac fresh pour qu'elle accepte une liste deGravatar herbelin2006-10-24
| | | | | | | noms et de chaînes qu'elle va concaténer pour créer un nom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9267 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #1194: normalisation evars a la sortie de focusGravatar barras2006-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9261 85f007b7-540e-0410-9357-904b9bb8a0f7
* affichage des ... dans les scriptsGravatar barras2006-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
| | | | | | | | apparaît dans le but ou dans l'une des hypothèses (ferme les bugs #447, #883 et #1228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9201 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
* improve the amount of information given by the Ltac tactic debuggerGravatar bertot2006-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
| | | | | | | | | | | | | | | | | | | Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵Gravatar herbelin2006-05-30
| | | | | | permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
| | | | | | | | | (i.e. cachées sous un nom de constante) sont considérées comme monomorphes. - Divers: renommage type_of_applied_inductive, un peu de documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection mode Debug On contre Ctrl-DGravatar herbelin2006-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8795 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-26 14:44:31 +0000