coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Changement des named_context	gregoire	2005-12-02
\| \| \| \| \| \| \| \|	Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage suite à la détection par défaut des variables inutilisées par ↵	herbelin	2005-11-08
\| \| \| \| \| \|	ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration type casted_open_constr pour tactique refine car l'unification ↵	herbelin	2004-12-09
\| \| \| \| \| \|	n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Garder les cast semble décidément le meilleur moyen de rester synchrone ↵	herbelin	2004-12-06
\| \| \| \| \| \|	avec l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6424 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des cast après avoir utiliser l'information de type (Tacinv ↵	herbelin	2004-12-06
\| \| \| \| \| \|	envoie à refine des métas castées avec des métas ?!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de la coercion vis à vis du but au niveau de Refine suite à ↵	herbelin	2004-12-06
\| \| \| \| \| \|	changement de CastedOpenConstr en OpenConstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ↵	herbelin	2004-12-06
\| \| \| \| \| \|	que de fonctions récursives même si l'une de ses fonctions n'a pas de meta); suppression gmm au passage suite commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug #787 de Roland	barras	2004-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug soumis par Yves	herbelin	2003-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5094 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
\| \| \| \| \| \| \| \| \|	Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 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
*	Simplification de Proof_type.prim_rule	herbelin	2002-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
\| \| \| \| \| \| \| \|	+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq-bugs #12: probleme de metamap resolu	barras	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2308 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat ocaml 3.03	filliatr	2001-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	GROS COMMIT:	barras	2001-11-05
\| \| \| \| \| \| \| \| \| \|	- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
*	let-in dans Refine	filliatr	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2013 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refine sur les CoFix	filliatr	2001-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1807 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin	2001-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de la structure des points fixes	barras	2001-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 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
*	bug de refine: uncaught exception Array.sub	barras	2001-03-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1443 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvelle implantation de la reduction	barras	2001-03-01
\| \| \| \| \| \| \|	suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression warning et calcule type dans replace_by_meta dans tous les cas	filliatr	2000-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1127 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression des (* open Generic *)	filliatr	2000-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 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@727 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique :	herbelin	2000-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	mise en page	herbelin	2000-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage AppL en App	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 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
*	Abstraction de constr	herbelin	2000-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction pour make doc	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de Abst	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
\| \| \| \| \| \| \|	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@590 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cosmétique	herbelin	2000-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@582 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	portage Refine	filliatr	2000-07-20
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7