aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-05-02Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ↵notin
Mimram) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Bug assert asherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8774 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-29suite de l'ajout des FSets/FMaps dans les theories standardsletouzey
-> OrderedTypeEx: des exemples de OrderedType -> OrderedTypeAlt: une definition alternative de OrderedType -> FSetAVL et FMapAVL: realisation a coup d'AVL -> FMapPositive: realisation a coup d'arbre binaire (selon les chiffres binaires de la cle) -> FMapIntMap : realisation en utilisant IntMap -> FSetToFiniteSet: un ensemble de FSet est un ensemble de Ensemble.v FSetAVL et FMapAVL prenent 30 secondes chacuns sur ma machine: on peut ne pas les compiler en passant l'option "-fsets no" a configure, de facon similaire a "-reals no" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8773 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-29meilleur nommage pour PairOrderedTypeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8772 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-29qq proprietes de plus sur Ncompareletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8771 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Continue l'écriture de la doc de "Function". Pas fini, manque:courtieu
- relecture par YB et JF - adaptation de la partie functional induction - écriture de la partie functional inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8770 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28If function creates proof obligation, there are now printed once.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8769 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28 r8931@thot: notin | 2006-04-28 16:19:38 +0200notin
Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8767 ↵notin
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8766 ↵notin
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8765 ↵notin
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8764 ↵notin
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8763 ↵notin
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8762 ↵notin
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Ajout bug #1102herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8761 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Standardisation du nom des méthodes de Evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Typo dans précédent commit (8755); protection renforcée dans analyse ↵herbelin
clause in du cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8757 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8756 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27- Distinction explicite des parties paramètres et arguments dans le typeherbelin
des inductifs de la clause "in" du filtrage. - Débogage et extension du parseur xml (g_xml.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Message d'erreur plus informatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8754 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Official MoWGLI definition of CIC dtdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8753 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Modification of emacs output: No more show script at the end of a proof.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8751 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Suppression de l'entrée devdoc dans le Makefile principal et modification ↵notin
en conséquence du Makefile dans dev/doc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8750 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Ajout de la doc de l'option -stdout de coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Modification of emacs output: Pp.warning and al now output warningcourtieu
between special characters. I had to add a hidden variable print_emacs and a function to set it to true in Pp because using Options.print_emacs would have introduce a circularity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8748 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Modification of emacs output: Pp.warning and al now output warningcourtieu
between special characters. I had to add a hidden variable print_emacs and a function to set it to true in Pp because using Options.print_emacs would have introduce a circularity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8747 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27préparation de add_glob en vue d'isolement de la partie module pourherbelin
l'option glob-dump git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8746 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Ajout chop_dirpathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8745 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-272-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8744 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Added a short doc for "Function". To be finished.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8743 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8742 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26- Utilisation d'abbréviations pour les types intervenant dans RCasesherbelin
- Factorisation du procédé de transformation Cases -> RCases dans Detyping - Rebranchement de la traduction XML pour Cases (interrompue depuis suppression traducteur) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8741 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Outil de test de la réversibilité du réafficheur v8->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8740 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Diverses corrections de l'afficheur et du traducteur pour s'assurer deherbelin
la réversibilité de la traduction (correction enregistrement des retours chariot dans le lexeur, correction affichage espace superflu en tête des VERNAC EXTEND, correction affichage morphism_signature dans extraargs.ml4, correction affichage clear dans pptactic.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8739 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Régénération après mise à jour coqdep pour traiter Require multipleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8738 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Prise en compte du Require multipleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8737 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26suite du pont entre Bvector et Nletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8736 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Replacing "GenFixpoint" with "Function" and "mes" with "measure"jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8735 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la ↵notin
création du fichier de style git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8734 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-25Un gros coup de lifting pour IntMap: letouzey
* le type ad des adresses est maintenant un alias vers le N de NArith, qui lui est isomorphe. * toutes les operations sur ces adresses (p.ex. un xor bit a bit) sont maintenant dans de nouveaux fichiers du repertoire NArith. * Intmap utilise maintenant le meme type option que le reste du monde * etc etc... Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs utilisant Intmap sont adaptees en consequence. Me demander si besoin ma moulinette d'adaptation (incomplete). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-25un lemme de double inclusionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8732 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-25Reverting nf_betaiotaevar_preserving_vm_castjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8731 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-25Code mort (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8730 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-25Suppression code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8729 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24Timide tentative de clarification du statut de l'opérateur de filtrageherbelin
PCase dans le type pattern: le type pattern est utilisé essentiellement dans ltac, il est normalement obtenu sans typage, et ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le type, il est impossible de savoir le nombre d'arguments du constructeur puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas dans la syntaxe concrète (résolution au passage du bug #1070, dû à un filtrage incomplet dans le passage de pattern à rawconstr permettant l'affichage des pattern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24Changement anomaly en failwith dans out_name pour utilisation par map_succeedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8727 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;herbelin
petites améliorations de l'afficheur de ltac match context (moins de parentheses, plus de structure) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8726 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24+ Handling "if" and cast in GenFixpoint jforest
+ Correcting a bug in recursives funcitons detection in GenFixpoint + Parially handling applied binders in funcitonal principles generation tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8725 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 17:36:36 +0000