aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Corrections dans le Print Assumption. Les definitions locales ("Let") Gravatar aspiwack2007-05-30
| | | | | | | | | | | | sont maintenant prises en compte (ca a l'air de marcher). En plus j'ai corrige l'ordre d'impression pour que ca imprime les noms dans l'ordre alphabetique (avant c'etait l'ordre inverse, etonnament perturbant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Memory optimisation for modules and constrs substitutions.Gravatar soubiran2007-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of (PR#1576).Gravatar soubiran2007-05-25
| | | | | | | | The construction of the resolver was bugged during the join operation of two substitutions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9858 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite restructuration unification et division des problèmesGravatar herbelin2007-05-23
| | | | | | | | | | | d'unification des types des with-bindings en deux: les problèmes d'unification susceptibles d'introduire une coercion sont retardés (comme dans le commit r9850) et ceux susceptibles de fournir d'autres instances restent faits au plus tôt (comme avant le commit r9850). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
* corrections bug dans l'implem de int31Gravatar bgregoir2007-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction partielle du bug #1388 (augmentation de la taille des code ↵Gravatar jforest2007-04-05
| | | | | | acceptes par la vm) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9747 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de la vm:Gravatar notin2007-03-27
| | | | | | | | | | | | | | | - le type val_kind n'embarque plus le constr (pb de cohérence avec le context); - en revanche, lors du calcul d'une valeur, on calcule aussi l'ensemble des variables nommées dont la valeur peut dépendre; - lors du clear_hyps, si la valeur dépend d'une variable effacée, on invalide le calcul. Corrige le bug #1419 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9733 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
* Removed some useless code in mod_typing that was redundant with safe_typing.Gravatar soubiran2007-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppresion de la catégorie des inductifs singletons larges dontGravatar herbelin2007-02-09
| | | | | | | | l'élimination vers Set était autorisée: comme souligné par Benjamin, c'est incompatible avec EM + AC (report rev 9633 8.1) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 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
* suite du commit 9557 Gravatar soubiran2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite correction sur un message d'erreur renvoyé au sous typage.Gravatar soubiran2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9557 85f007b7-540e-0410-9357-904b9bb8a0f7
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
| | | | | | | de deux signatures de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9531 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
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
| | | | | | | | | les interfaces de module (bug similaire à #1302 mais pour les définitions -- au lieu des inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1302Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 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
* cosmetiqueGravatar barras2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9442 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
* 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
* 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
* dependencesGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9320 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
* Ajout fold_rel_declaration et fold_named_declarationGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de 2 bugs critiques du polymorphisme d'universGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9301 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification des contraintes sur le contexte de paramètres desGravatar herbelin2006-10-17
| | | | | | | | | | | inductifs dans le test de sous-typage (exigence du même nombre d'arguments uniformes attendus mais pas d'exigence spéciale sur les définitions locales du contexte à partir du moment où les types et constructeurs sont convertibles quand généralisés par rapport au contexte de paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection raise en début de séquence (en attendant que le code caché ↵Gravatar herbelin2006-10-12
| | | | | | trouve sa place) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
| | | | | | | | vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug #1242) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 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
* Correction du bug #1181Gravatar jforest2006-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indentation + typoGravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout iter_rel_context/iter_named_contextGravatar herbelin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Appel à caml_modify pour Ocaml 3.07Gravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de closedn pour EvarutilGravatar herbelin2006-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9086 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug vm_computeGravatar bgregoir2006-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans les scripts de configuration (coqtop et coqide affichent ↵Gravatar notin2006-07-28
| | | | | | maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 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 bug du polymorphisme de sort des inductifs (cas où les variables ↵Gravatar herbelin2006-06-22
| | | | | | d'univers associées aux arités des paramètres ne sont pas distinctes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oh le joli bug dans le kernel:Gravatar letouzey2006-06-05
| | | | | | | | | | | | | | | | | Definissons un foncteur dependant de X et Y. Alors: Module M : Funsig (X : T) Funsig (Y : T) Sig End := Functor [Y:T] Functor [X:T] Struct End Notez les places de X et Y, a cause d'un fold_right qui aurait du etre gauchiste. Etonnement, tout marchait tres bien en Coq, donc ce bug a survecu discretement depuis l'ajout initial des modules. Avant que je n'essaie d'extraire un foncteur a deux arguments... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8898 85f007b7-540e-0410-9357-904b9bb8a0f7
* retour au comportement antérieur pour une application de foncteur: Gravatar letouzey2006-05-30
| | | | | | | | | | plus d'expansions, un foncteur F dependant de X donne une fois appliquee a M un module dont le corps est simplement celui de F avec des M a la place des X. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8879 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 07:21:15 +0000