coq - The formal proof system

Age	Commit message (Collapse)	Author
2001-03-15	entetes	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12	syntaxe 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-11-23	Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@924 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20	Ajout pr_global_reference et is_visible	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@856 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec ↵	herbelin
	sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@728 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18	Renommage canonique :	herbelin
	declaration = definition \| assumption mode de reference = named \| rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifierconstrtyped_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@485 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-26	Modification messages d'erreurs, possibilité de n'importe quel constr dans ↵	herbelin
	les instances de références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28	Déplacement du type reference dans Term	herbelin
	Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@384 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26	Introduction d'un type constr_pattern pour les différents filtrages	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@371 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-31	Export gentermpr avec renommage	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@290 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07	Restructuration printer et parser	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@263 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
	les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09	Ajout des messages d'erreurs de Cases	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@226 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03	modules profile, Coqinit et Coqtop (=main)	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01	Ajout des fonctions prpattern et prrawterm	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@184 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01	printers	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@174 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26	module Pretty (partiellement)	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@150 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26	module Extend	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@142 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-13	organisation de trad (entre parsing/ et pretyping/)	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@102 85f007b7-540e-0410-9357-904b9bb8a0f7