coq/contrib/correctness, branch master

Cleanup: remove old correctness files, unused for a long time

2009-03-11T13:36:35+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11971 85f007b7-540e-0410-9357-904b9bb8a0f7

Suppression de la partie ML de la contrib correctness. Les fichiers

2008-04-29T13:47:57+00:00

n'étaient plus compilés depuis le 14 janvier 2004 (avant la 8.0), Why
ayant pris la suite de correctness.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10870 85f007b7-540e-0410-9357-904b9bb8a0f7

Correction du bug des types singletons pas sous-type de Set

2008-04-27T16:46:15+00:00

(i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le
principe de la hiérarchie d'univers est d'être cumulative -- et que
Set en soit le niveau 0).

Une solution aurait été de poser Prop <= Set mais on adopte une autre
solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type
et Prop <= Set, on garde la représentation de Prop au sein de la
hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau
sans aucune contrainte inférieure, appelons Type -1) et on adapte les
fonctions de sous-typage et de typage pour qu'elle prenne en compte la
règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets
incidents dans Termops.refresh_universes et Univ.super).

Petite uniformisation des noms d'univers et de sortes au passage
(univ.ml, univ.mli, term.ml, term.mli et les autres fichiers).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7

Plus de combinateurs sont passés de Util à Option. Le module Options

2007-12-06T17:36:14+00:00

devient Flags.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7

Factorisation des opérations sur le type option de Util dans un module

2007-12-05T21:11:19+00:00

lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting 
des fonctions (à un ou deux arguments tous ou partie de type option).

Il reste quelques opérations dans Util à propos desquelles je ne suis 
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain 
car il est tard (comme some_in qui devrait devenir Option.make je 
suppose) . Elles s'expriment souvent facilement en fonction des 
autres, par exemple "option_compare x y"  est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est 
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.

J'en ai profité aussi pour remplacer les trop nombreux "failwith" par 
des erreurs locales au module, donc plus robustes.

J'ai trouvé aussi une fonction qui était définie deux fois, et une 
définie dans un module particulier.

Mon seul bémol (mais facile à traiter) c'est la proximité entre le 
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de 
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7

useless Require Export Extraction

2007-11-06T01:27:17+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10290 85f007b7-540e-0410-9357-904b9bb8a0f7

Suppression des type_app et body_of_type qui alourdissent inutilement le code

2007-08-27T11:41:08+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7

Generalized CAMLP4USE for pp dependencies

2007-07-16T09:18:44+00:00

Removed parsing/lexer.ml4 special case
No file depends on pa_extend_m.cmo anymore, Wierd ...


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7

Standardisation du nom des méthodes de Evd

2006-04-28T12:24:14+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7

Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des 'properties' de Subversion

2006-04-28T10:34:25+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7