aboutsummaryrefslogtreecommitdiff
path: root/library/impargs.ml
AgeCommit message (Collapse)Author
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter ↵herbelin
les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@485 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03suppression de Fw pour les implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@405 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@363 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12modulesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02modifs pour premiere edition de liensfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01poursuite de Vernacentriesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@178 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01 - environment -> safe_environmentfilliatr
- unsafe_env -> env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01 - Typing -> Safe_typingfilliatr
- proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26module Termastfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@149 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-18 - déplacement (encore une fois !) des variables existentielles : elles sontfilliatr
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
1999-09-28juste l'interface de Dischargefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@85 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-19 - un effort sur la doc (ocamlweb)filliatr
- 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 23:01:40 +0000