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
*	Confusion assert/error détectée par nouveau warning X de ocaml 3.09	herbelin	2005-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection against saving a proof with still non-instantiated evars (cf bug ↵	herbelin	2005-04-29
\| \| \| \| \| \|	#901) (continued!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6975 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection against saving a proof with still non-instantiated evars (cf bug ↵	herbelin	2005-04-29
\| \| \| \| \| \|	#901) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵	herbelin	2004-12-31
\| \| \| \| \| \|	Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en page	herbelin	2004-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6322 85f007b7-540e-0410-9357-904b9bb8a0f7
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	hiding the meta_map in evar_defs	barras	2004-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement de clenv vers pretyping	barras	2004-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
*	premiere reorganisation de l\'unification	barras	2004-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 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
*	added breakpoints to help ide	corbinea	2004-02-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug affichage des metas dans un environnement avec definitions locales (bug 277)	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5116 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	2 espaces en trop	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4812 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration de l'afficheur de script structure	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4797 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ground update	corbinea	2003-07-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4227 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ground Update.	corbinea	2003-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 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
*	Affichage des tactiques en v8	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3865 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
\| \| \| \| \| \| \| \| \|	pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un message à FailTac	herbelin	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
\| \| \| \| \| \| \| \| \| \| \|	- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre l'encapsulage de FailError dans Exc_located (sinon, par ↵	herbelin	2002-07-11
\| \| \| \| \| \|	exemple, 'Try Tauto' ne marche pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2855 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation des tclTHEN (cf dev/changements.txt)	herbelin	2002-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2721 85f007b7-540e-0410-9357-904b9bb8a0f7
*	prterm -> prterm_env	filliatr	2002-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2463 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
*	suppression de l'affichage des noeuds Change_evars	barras	2001-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2289 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 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
*	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
*	Problème d'affichage d'un . pour les Local_constraints; remplacement par Idtac	herbelin	2001-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2047 85f007b7-540e-0410-9357-904b9bb8a0f7
*	exceptions	barras	2001-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1965 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'affichage du non-reparsable 'Local constraint change'	herbelin	2001-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1865 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
\| \| \| \| \| \| \|	ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Metas dans les Unfold's	delahaye	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1607 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reparation du bug de Try	delahaye	2001-04-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1591 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
*	introduction d'un refine avec resolution des types et de l'instantiation des ↵	mohring	2001-02-28
\| \| \| \| \| \|	metas dans les existentielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification du make depend; fonctions de stat. util. memoire dans ↵	filliatr	2001-02-08
\| \| \| \| \| \|	certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de debug en assert	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1206 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints ↵	herbelin	2000-12-20
\| \| \| \| \| \|	qui fait l'instantiation des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hint Unfold Local + commentaires	mohring	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1088 85f007b7-540e-0410-9357-904b9bb8a0f7