aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* - module Redinfo dans library/ pour les constantes d'éliminationGravatar filliatr1999-10-22
| | | | | | | - module Tacred : fonctions de reductions utilisees dans les tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@114 85f007b7-540e-0410-9357-904b9bb8a0f7
* - documentation repertoire proofs/Gravatar filliatr1999-10-20
| | | | | | | | - IsAppL of constr * constr list ==> répercussion - module Clenv (suite; as terminé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Clenv (debut)Gravatar filliatr1999-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@111 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Evar_refiner et Typing_evGravatar filliatr1999-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
| | | | | | | | unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres le module Environ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@108 85f007b7-540e-0410-9357-904b9bb8a0f7
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
| | | | | | | | | | toujours dans le noyau (en ce sens que Reduction et Typeops les connaissent) mais dans un argument supplémentaire A COTE de l'environnement (de type unsafe_env) - Indtypes et Typing n'utilisent strictement que Evd.empty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@106 85f007b7-540e-0410-9357-904b9bb8a0f7
* module LogicGravatar filliatr1999-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Proof_treesGravatar filliatr1999-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@104 85f007b7-540e-0410-9357-904b9bb8a0f7
* plus de recettes pour les corps des constantesGravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@100 85f007b7-540e-0410-9357-904b9bb8a0f7
* - re-introduction d'une evar_map dans unsafe_envGravatar filliatr1999-10-13
| | | | | | | - les var. ex. sont des entiers, et non plus des section_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@99 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentationGravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@98 85f007b7-540e-0410-9357-904b9bb8a0f7
* redeplacement des var. ex. dans kernel :-)Gravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@97 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@93 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout des constraintes pendant le chargement d'un module (load)Gravatar filliatr1999-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@81 85f007b7-540e-0410-9357-904b9bb8a0f7
* message erreur UI pendant importGravatar filliatr1999-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@79 85f007b7-540e-0410-9357-904b9bb8a0f7
* ensembles de contraintes d'universGravatar filliatr1999-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
| | | | | | | | | - module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
* module LibraryGravatar filliatr1999-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7
* affichage des erreurs de typage dans minicoqGravatar filliatr1999-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@73 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules System, Lib et StatesGravatar filliatr1999-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@71 85f007b7-540e-0410-9357-904b9bb8a0f7
* les sections ne sont plus stockées à l'envers dans les section pathsGravatar filliatr1999-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@70 85f007b7-540e-0410-9357-904b9bb8a0f7
* - deplacement time stamps dans System (car utilise Unix)Gravatar filliatr1999-09-08
| | | | | | | - dependances fichiers camlp4 (quelle merde !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@56 85f007b7-540e-0410-9357-904b9bb8a0f7
* - bug: une fois typés, les arités des constructeurs étaient rangéesGravatar filliatr1999-09-07
| | | | | | | en ordre inverse (fold_left au lieu de fold_right) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@44 85f007b7-540e-0410-9357-904b9bb8a0f7
* - minicoq : definition inductifs; syntaxe a->bGravatar filliatr1999-09-07
| | | | | | | | - kernel : bug Typing/one_inductive (il fallait chercher l'arite typée dans l'environnement avec lookup_rel et non lookup_var) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@43 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place commandes minicoqGravatar filliatr1999-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@42 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place repertoire test-suite/, toplevel/, parsing/Gravatar filliatr1999-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@39 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Libobject et Summary (partiel)Gravatar filliatr1999-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@36 85f007b7-540e-0410-9357-904b9bb8a0f7
* - environnements videsGravatar filliatr1999-09-03
| | | | | | | | - suppression du constructeur Implicit (et IsImplicit du coup) - nettoyages divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@35 85f007b7-540e-0410-9357-904b9bb8a0f7
* typage constructeur :Gravatar filliatr1999-08-30
| | | | | | | | | on ajoute les contraintes d'univers en typant l'arité c d'un constructeur en mettant les paramètres p dans l'environnement, et non pas en typant le produit (p)c. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@34 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout des inductifs (sans types singletons pour l'instant)Gravatar filliatr1999-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@32 85f007b7-540e-0410-9357-904b9bb8a0f7
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression champs inutiles dans constantes et inductifs; verification ↵Gravatar filliatr1999-08-27
| | | | | | definitions inductives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@29 85f007b7-540e-0410-9357-904b9bb8a0f7
* environnement surGravatar filliatr1999-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@28 85f007b7-540e-0410-9357-904b9bb8a0f7
* mach -> typing; machops -> typeopsGravatar filliatr1999-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@27 85f007b7-540e-0410-9357-904b9bb8a0f7
* - abstractionGravatar filliatr1999-08-26
| | | | | | | | | - univers fonctionnels - erreurs de typage maintenant sous forme d'exception, déclarées dans Type_errors git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@24 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Instantiate, Constant et InductiveGravatar filliatr1999-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@22 85f007b7-540e-0410-9357-904b9bb8a0f7
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@21 85f007b7-540e-0410-9357-904b9bb8a0f7
* - suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujoursGravatar filliatr1999-08-23
| | | | | | | | ajustés - déplacement du type pb_conv dans Reduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@20 85f007b7-540e-0410-9357-904b9bb8a0f7
* programmation literaire : un fichier de description par repertoireGravatar filliatr1999-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@19 85f007b7-540e-0410-9357-904b9bb8a0f7
* machine: execute = typage avec universGravatar filliatr1999-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@18 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place programmation literaire (generation de doc/coq.tex)Gravatar filliatr1999-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Reduction (fin)Gravatar filliatr1999-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Reduction (debut)Gravatar filliatr1999-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12 85f007b7-540e-0410-9357-904b9bb8a0f7
* module ClosureGravatar filliatr1999-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11 85f007b7-540e-0410-9357-904b9bb8a0f7
* generic, term et evdGravatar filliatr1999-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9 85f007b7-540e-0410-9357-904b9bb8a0f7
* ancien names decoupe en names + signGravatar filliatr1999-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6 85f007b7-540e-0410-9357-904b9bb8a0f7
* Initial revisionGravatar filliatr1999-08-16
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 20:56:07 +0000