coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Messages d'erreurs Cases	herbelin	2000-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction incompatibilites dans la fn des types des inductifs	herbelin	2000-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs de la réduction de Fix dans Simpl	herbelin	2000-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle stratégie de nommage dans Simpl pour Fix	herbelin	2000-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@653 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau bug dans la réduction de Fix par red_elim_const	herbelin	2000-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@648 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
*	Renommage AppL en App; Suppression cast	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de whd_castapp	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@627 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renommage map_constr_with_named_binders	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@625 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Disparition du type oper mais nouveau type global_reference	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement 'a reference et binder_kind de Term vers Rawterm	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@619 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
*	Minor correction for Ocamlweb + doc update	coq	2000-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@608 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
*	Déplacement de fonctions de Reduction vers Tacred	herbelin	2000-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@603 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
*	Vers la paramétrisation des fonctions de Reduction et vers la fusion de	herbelin	2000-09-12
\| \| \| \| \| \| \|	Closure.stack avec une nouvelle abstraction des 'stacks' de Reduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@596 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@591 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
*	kernel/type_errors.ml	herbelin	2000-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@583 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation bug des coercions (cas ou on importe une coercion faisant	barras	2000-08-08
\| \| \| \| \| \| \|	reference a une classe non importee) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@577 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
*	Modifs d'interpretation de patterns	delahaye	2000-07-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@562 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
*	Plus de env et sigma dans get_arity, plus de sigma dans make_arity	herbelin	2000-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@546 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de find_inductive aux co-inductifs et renommage en find_rectype	herbelin	2000-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@542 85f007b7-540e-0410-9357-904b9bb8a0f7
*	index devenu list_index échoue maintenant avec Not_found et plus Failure	herbelin	2000-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@540 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de find_inductive aux co-inductifs et renommage en find_rectype	herbelin	2000-07-01
\| \| \| \| \| \| \| \|	Contournement des dépendances de Rel dans les Evar pour l'inférence du prédicat (erreur "TODO4-1") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_of	herbelin	2000-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@532 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Séparation des contraintes de type et de valeur dans pretyping	herbelin	2000-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@531 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bricoles	herbelin	2000-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de l'inférence des types des lambdas du prédicat	herbelin	2000-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@524 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Achèvement abstraction du mécanisme (optionnel) de cast	herbelin	2000-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rattrapage d'un Not_found pour les VAR's.	delahaye	2000-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@519 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs	herbelin	2000-06-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration messages erreurs	herbelin	2000-06-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@502 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs infrence des arguments manquants dans le prdicat	herbelin	2000-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs et simplification (suite)	herbelin	2000-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs et simplifications coercions	herbelin	2000-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@487 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Afficahge des locations	herbelin	2000-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@483 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de Generic	herbelin	2000-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification messages d'erreurs, possibilité de n'importe quel constr dans ↵	herbelin	2000-05-26
\| \| \| \| \| \|	les instances de références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug existential_value au lieu de existential_type + divers sur existential	herbelin	2000-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de cast	herbelin	2000-05-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rien	herbelin	2000-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls	herbelin	2000-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7