aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* retablissement du toplevelGravatar filliatr1999-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@83 85f007b7-540e-0410-9357-904b9bb8a0f7
* module DeclareGravatar filliatr1999-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 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
* 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
* documentation repertoire toplevelGravatar filliatr1999-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@72 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Himsg, comme un foncteurGravatar filliatr1999-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@64 85f007b7-540e-0410-9357-904b9bb8a0f7
* minicoq: pretty-print applications; ambiguite grammaire supprimee; Ind, ↵Gravatar filliatr1999-09-08
| | | | | | Const et Construct mots cles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@51 85f007b7-540e-0410-9357-904b9bb8a0f7
* instanciation des opérateurs sur la bonne signature (celle deGravatar filliatr1999-09-07
| | | | | | | | définition, puisqu'elle ne peut pas changer, mais qu'elle peut être un préfixe) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@45 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
* (debut) de grammaire minicoqGravatar filliatr1999-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@41 85f007b7-540e-0410-9357-904b9bb8a0f7
* un mini toplevel pour tester le noyauGravatar filliatr1999-09-06
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@38 85f007b7-540e-0410-9357-904b9bb8a0f7