aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-02-08one forgotten compatibility lemmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10526 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Oubli dans r10524notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10525 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Correction d'un bug de Coqdoc + ajout de Include dans les mots clés ↵notin
reconnus par Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10524 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-07Mise en place d'une toute petite amélioration de l'unification deherbelin
apply : si on a trouvé une méta, alors, on l'utilise pour instancier les trous lors de la tentative de conversion modulo delta. Cela permet ainsi de résoudre de petits cas d'unification, tel que celui annoncé échouant dans le "beginner question" du 6 fevrier 2008 de coq-club. Solde au passage de modifs cosmétiques de setoid_replace.ml avant abandon probable du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10523 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Suite 10518herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10521 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06- Documentation des nouvelles options d'implicites (Set Strongly Strictherbelin
Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de Set Strongly Strict Implicit : il contient maintenant Set Strict Implicit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Détection plus souple et message un peu moins radical en cas deherbelin
fichiers emacs ouverts au moment de la création des dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10519 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Correction d'un bug à l'interprétation de "change" (on exigeait queherbelin
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
2008-02-06Résolution d'une confusion dans le rôle des variables CAMLP4 et CAMLP4LIB:herbelin
- CAMLP4 dit si on utilise camlp4 ou camlp5 - CAMLP4LIB est le chemin camlp4/5 à donner en option -I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10517 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Fix obligations not being discharged due to new definition of complement.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10516 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Work-in-progress to make eauto accept a list of goals as input andmsozeau
return a solution for the whole set of goals at once only. Add "debug eauto" and "dfs eauto" syntaxes to get better control on the algorithm from the surface interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10514 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Protection contre l'erreur mentionnée dans le rapport de bug 1790herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10513 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05kill some useless module aliases E:=X (for better name printing, see Elie's ↵letouzey
14097) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Correction d'un bug sur les substitutions:soubiran
Require Import FSets FSetAVL. Module M:=FSetAVL.Make Z_as_OT. (* ... uncaught exception Not_found *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10509 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Add Morphisms for Qceiling and Qfloorroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10508 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Ajout d'un test pour le bug #1787notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10507 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
Thanks to Elie's work and especially "Include Type ...", full sets can be simply expressed as extensions of weak sets. Moreover, Facts and Properties functors can be factorized almost completely. As a result, things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB, Same with maps / weak maps ... No backward compatibility intended for weak sets / maps, but porting scripts should mostly amounts to name changes (see above). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10505 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-04Instantiation of evars after instantiate (closes #1672).glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10504 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-04declaremods.mlsoubiran
Patch function load_include git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10503 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
for basic functional programming and relation definitions respectively. Classes.Relations also includes the definition of Morphism and instances for the standard morphisms and relations (eq, iff, impl, inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic has been reimplemented on top of these definitions, hence it doesn't require a setoid implementation anymore. It also generates obligations for missing reflexivity proofs, like the current setoid_rewrite. It has not been tested on large examples but it should handle directions and occurences. Works with in if no obligations are generated at this time. What's missing is being able to rewrite by a lemma instead of a simple hypothesis with no premises. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-02fix the syntax "Include Type Foo"letouzey
I dont precisely understand what's going on, but it definitively works better after my fix (copied from the Module / Module Type settings). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10501 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide ↵letouzey
(from A. Bohannon) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10500 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Ajout de 2 testsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10499 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Thanks to Elie, we can share duplicated stuff in FSets: for a start, ↵letouzey
FSetWeakFacts and FSetFacts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10498 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
kernel: -declaration.ml unification des representations pour les modules et modules types. (type struct_expr_body) -mod_typing.ml le typage des modules est separe de l'evaluation des modules -modops.ml nouvelle fonction qui pour toutes expressions de structure calcule sa forme evaluee.(eval_struct) -safe_typing.ml ajout du support du nouvel operateur Include.(add_include). library: -declaremods.ml nouveaux objets Include et Module-alias et gestion de la resolution de noms pour les alias via la nametab. parsing: -g_vernac.ml4: nouvelles regles pour le support des Includes et pour l'application des signatures fonctorielles. extraction: Adaptation a la nouvelle representation des modules et support de l'operateur with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Suite révision 10495herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10496 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
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
2008-01-31Fix obvious syntax error. Forgot to recompile before commiting...msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10493 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Remove unneeded .d mask, can be set localy by each dev inmsozeau
~/.subversion/config global-ignores git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10492 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Ignore generated dependency files.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10491 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Debug implementation of dependent induction/dependent destruction and ↵msozeau
document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Finish let| implementation and document itmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Support for occurences and 'in' in class_setoid, work on corresponding ↵msozeau
tactics in SetoidClass git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10486 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Use new redefinition support for the default obligations tacticmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10485 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Support for substructures in classes using :> notationmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10484 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Add occurence extra argmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10483 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Debug 0-ary typeclasses support, use new redefinition support for default tacticmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10482 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Add list_iter3 msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10481 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Add some keywordmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10480 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-29Added full documentation for mathematical mode (draft version)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10479 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-29Correction du bug #1785notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10478 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Nicer proofs.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10476 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24remove Fourier Failure warnings.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10474 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Prove the decidability of arithmetical statements using the real numbers.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10473 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Fermeture du bug #1754notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10472 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Keep the Z_scope local to this file.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10471 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-23Changing R to a local definition so that it isn't exported.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10470 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-23Ajout d'un test pour le bug #1779notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10468 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:03:29 +0000