coq - The formal proof system

Age	Commit message (Expand)	Author
2005-06-09	backtrack sur le typage des instantiations d\'evars	barras
2005-06-08	evar declarees avec mauvais type	barras
2005-06-07	pas de filtrages partiels	barras
2005-06-07	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras
2005-06-06	essai de typage des instantiations d\'evars	barras
2005-06-05	eradication de Evarutil.w_Define	barras
2005-06-05	assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...	barras
2005-05-28	unification: evar_define checks the free variables are bound in the evar context	barras
2005-05-25	Added subtac contrib.	coq
2005-05-24	Added clenv_environments_evars that behaves as clen_environments but	sacerdot
2005-05-24	WARNING: unification changed (to fix a bug).	sacerdot
2005-05-20	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin
2005-05-20	Documentation	herbelin
2005-05-19	A wish by Bas Spitters granted: a little more of unification up to	sacerdot
2005-04-29	Fix bug in prepare_predicate_from_tycon; improved error message when no claus...	herbelin
2005-03-15	Backtrack sur la substitution combinée avec l'instanciation en réponse à l...	herbelin
2005-03-12	Backtrack version 1.82 awaiting for better understanding of the consequences ...	herbelin
2005-03-11	Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...	herbelin
2005-03-10	A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...	herbelin
2005-03-10	A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...	herbelin
2005-03-09	bug #931 (continued): no recursion on the evars instantiation	herbelin
2005-03-08	Fix bug #931: leave dependent evars as such for refine	herbelin
2005-03-08	Ajout fold	herbelin
2005-03-01	Code mort	herbelin
2005-02-18	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin
2005-02-18	Standardisation of function names about global references (especially, renami...	herbelin
2005-02-18	Moving subst_inductive from tacinterp to inductiveops for better for reuse in...	herbelin
2005-02-18	Ajout it_mkNamedProd_wo_LetIn	herbelin
2005-02-18	Ajout splay_lambda	herbelin
2005-02-12	Uniformisation de destApplication en destApp	herbelin
2005-02-12	Ajout Print Canonical Structures	herbelin
2005-02-02	Correction de la précédence des contexts de variables rel, ltac et var	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-14	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot
2005-01-03	HUGE COMMIT	sacerdot
2005-01-02	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin
2004-12-29	ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...	herbelin
2004-12-29	Bug control_only_guard	herbelin
2004-12-09	Correction du bug de build_initial_predicate a révèlé un autre bug dans ex...	herbelin
2004-12-09	Achèvement correction bug do_restrict_hys: ne pas inverser les arguments	herbelin
2004-12-08	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin
2004-12-08	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin
2004-12-08	Bugs dans la déclaration du type du terme filtré si non défini	herbelin
2004-12-08	Bug nom exception	herbelin
2004-12-07	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot
2004-12-06	Relâchement obligation d'une contrainte de type sur les Hole en position ter...	herbelin
2004-12-06	C'est trop compliqué de mettre à jour les types du metamap en passant sous ...	herbelin
2004-12-06	Commentaire	herbelin
2004-12-03	Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...	herbelin