aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-06-07petites corrections dans la doc de functional xxx. courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8915 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Nouveaux Parametres Inductifscpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8914 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Réparation coqtop.mlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8913 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Changement de l'option -where: on vérifie si la variable d'environnement ↵notin
COQLIB est définie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8912 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07functional induction can now be used with jforest
using <principle> with <bindings> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8911 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07mise en texttt d'une commande.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8909 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Changements sur Functional xxx. Plus précis et plus exact.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8908 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06Ajout de précisions dans la doc de functional scheme et consort +courtieu
adaptation à la nouvelle version (syntaxe + sémantique). Reste Functional Scheme. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8905 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06this time it's good jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8904 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06Error in last commit jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8903 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06Debut modif parametres inductifs CICcpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8902 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06protecting an uncaught exception Not_found jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8901 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06reparation pour le bug #1072 (soufflee par J. Forest): letouzey
protection d'un list_chop pour couvrir le cas d'une application partielle de morphisme. accessoirement, il faudrait comprendre un jour pourquoi setoid replace inspecte (and True) dans le terme (map (and True) True <-> A) si on lui dit de reecrire A en autre chose... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8900 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06+ ameliorating the tactic "functional induction"jforest
+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-05Oh le joli bug dans le kernel:letouzey
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
2006-06-05Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome ↵letouzey
d'extensionalite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8897 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-05nouveaux parametrescpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8896 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-04MAJ svn:ignore coqc.opt et coqmktop.optherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8895 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-04Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict ↵herbelin
with FSets git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8894 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8893 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-02debut de reparation du test d'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8891 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01Update Program/subtac documentation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8890 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01Fix some nasty bug with the evars-to-dependent sum encoding.msozeau
Also enclose traces with try with clauses to avoid detypinging anomalies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8889 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01bug in alpha-conversionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8888 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01reparation bug #1128letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8886 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8885 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8884 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31ajout de QArith dans les theories standardsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8883 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31petits ajoutsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8882 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Replacing the old version of "functional induction" with the new one. jforest
The old version is, for now, still available by prefixing any command/tactic with Old/old (eg. old functional induction ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8881 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Colorisation dans Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8880 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30retour au comportement antérieur pour une application de foncteur: letouzey
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
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵herbelin
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
2006-05-30Correction bug #990 (LoadPath et option -R de coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8877 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30* suite de la revision des wrappers Makeletouzey
* quelques unfold E.eq en cas de changement de la semantique des foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8876 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29The "clean integration of subtac" patch.msozeau
Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29Fix broken paths.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8874 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29small changes jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8873 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8872 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28- Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesherbelin
(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
2006-05-28Adaptation au passage de sig2 dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8870 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28Adaptation au passage de vector dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8869 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28Adaptation au passage de option dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8868 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28Ajout array_fold_map2Ã'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8867 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26Modification de la compilation de coqc et coqmktop pour éviter le problème ↵notin
de stripping automatique sous Fedora git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8865 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26Added contrib/funind to the path for ocamldebug-coqcourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8864 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26Support des modules dans Coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8863 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26removing a warningjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8862 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:43:18 +0000