coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
\| \| \| \| \| \| \| \| \| \|	par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	types vs constr	herbelin	2001-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de dynamiques pour les quotations constr et tactic	delahaye	2001-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place globalisation optionnelle pour Infix/Distfix	herbelin	2001-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2046 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵	herbelin	2001-09-19
\| \| \| \| \| \|	des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵	herbelin	2001-09-10
\| \| \| \| \| \|	éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1946 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration de la structure des univers	barras	2001-03-28
\| \| \| \| \| \| \| \|	elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un système optionnel de discharge immédiat; prise en ↵	herbelin	2001-02-14
\| \| \| \| \| \|	compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1388 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ré-introduction des implicites à la volée dans la définition des inductifs	herbelin	2001-01-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1279 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation autour de globalize_constr	herbelin	2000-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@952 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵	herbelin	2000-11-22
\| \| \| \| \| \|	'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Acceptation des noms qualifiés; utilisation de global_reference dans ↵	herbelin	2000-11-20
\| \| \| \| \| \|	pattern; prise en compte des noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@881 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplifications autour de typed_type (renommé types par analogie avec ↵	herbelin	2000-10-18
\| \| \| \| \| \|	sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@728 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage	herbelin	2000-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@717 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement "command" en "constr" et globalize_command en globalize_constr	herbelin	2000-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@711 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reorganisation des interp_constr	herbelin	2000-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion ↵	herbelin	2000-09-26
\| \| \| \| \| \|	de 'OpenConstr' constitué d'un terme avec Métas et d'une liste de types pour les métas git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@615 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Canonisation de certains noms dans Pretyping, Asterm et Safe_typing	herbelin	2000-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifs d'interpretation de patterns + exceptions dans le lexer	delahaye	2000-07-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout interp_sort	herbelin	2000-05-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du langage de tactiques	delahaye	2000-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement du type reference dans Term	herbelin	2000-04-28
\| \| \| \| \| \| \| \| \|	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
*	Introduction d'un type constr_pattern pour les différents filtrages	herbelin	2000-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@371 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réajout globalize_command	herbelin	2000-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en ↵	herbelin	2000-03-28
\| \| \| \| \| \|	interp_constr etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@356 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise au point lexer / debugage PP	filliatr	1999-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@205 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- global_reference traite des variables	filliatr	1999-12-03
\| \| \| \| \| \| \| \| \|	- construct_reference, avec environnement en argument - link de Class - Definition et Check au toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@193 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs pour premiere edition de liens	filliatr	1999-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Egrammar	filliatr	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@176 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- environment -> safe_environment	filliatr	1999-12-01
\| \| \| \| \| \| \|	- unsafe_env -> env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 85f007b7-540e-0410-9357-904b9bb8a0f7
*	portage Astterm (partiellement)	filliatr	1999-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification pour faire compiler pretyping.ml qui maintenant compile	herbelin	1999-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@156 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ pour fusion avec pretyping	herbelin	1999-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
*	organisation de trad (entre parsing/ et pretyping/)	filliatr	1999-10-13
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@102 85f007b7-540e-0410-9357-904b9bb8a0f7