aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-07type attribute added to PROD (for ForAll vs Pi rendering)sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1081 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-07COPYRIGHT file added; some comments changedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1080 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Bug identarg au lieu de qualidargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1075 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Inner types are now reduced and arrows are created whensacerdot
products have dummy binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1050 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-01LETIN now has a letintarget instead of a targetsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1042 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-01cictypes.dtd changedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1041 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-30Used a force function to force stream evaluation only for aestaetics reasons.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1040 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-30Identifier order in the inner-types file changed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1039 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Changement dans les noms longs (2eme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1028 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Changement dans les noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1027 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Modifications due to the new As option in AddPath and AddRecPath.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1026 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Nouveau long long avec Coq en têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1020 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Nouveau long long avec Coq en têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1015 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Now also inner-types are exported.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1010 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Code clean-up due to the new usage of longer names in Coq.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1006 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath ↵herbelin
pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Many improvements. Xml contrib retached to the V7.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@994 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Appel des constantes globaux par des noms absolusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@966 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon ↵filliatr
Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Simplification de l'accès aux globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@933 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23id_of_global devient sp_of_globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@928 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵herbelin
'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21implicites manuelsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Remplacement des hacks pour les noms longs par un appel à ↵herbelin
Declare.global_qualified_reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@871 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15Changed the semantics of AddRecPath.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@852 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15methode exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵herbelin
library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@839 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09Renommage canonique SectionLocalDecl -> SectionLocalAssumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08nouveau load pathfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08First version with out_variable used. Exports all the standard librarysacerdot
without need of patches. Untested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@824 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Nettoyage Names suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@818 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Correction sur commit errone de la version 1.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@815 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@814 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵filliatr
constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03Few OCaml files in contrib/xmlsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@798 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03URI problem addressed, but not resolved yetsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@796 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Simpl fait trop maintenant; faut adapterherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@778 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Semi_Ring_Theory_of decommentemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@767 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@765 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26ntrefiner.ml* removed in module xmlsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Manquait le cas Constr de dyn_polynomherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@761 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Porting from V6 finished, but not working.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@759 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Added xml contribution to configuresacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@758 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25xml contribution created.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@756 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Changement des analyseurs syntaxiques de Grammar et Syntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@754 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Syntaxe des tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@752 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Renommage command -> constr et changement des analyseurs syntaxiques de ↵herbelin
Grammar et Syntax git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@751 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-14 00:28:57 +0000