coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	maj	filliatr	2004-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5364 85f007b7-540e-0410-9357-904b9bb8a0f7
*	makes sure the following examples are well-treated:	bertot	2004-02-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Export X. conditional trivial rewrite nat_le_correct in H. firstorder. Definition error := @None. Proof with trivial. Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l with minus := Rminus div := Rdiv. Ltac ElimPcompare c1 c2 := let x := fresh H in intro x. simplify_eq H. Extraction Inline list_length_induction. Extraction NoInline code insert isort map frequency_list huffman encode decode. ajoute une modification dans le traitement de let_tuple git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5363 85f007b7-540e-0410-9357-904b9bb8a0f7
*	files from contrib/interface need files from contrib/field, the variable	bertot	2004-02-19
\| \| \| \| \| \| \|	LOCALINCLUDES needs to contain -I contrib/field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5362 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs/insuffisances trouvees en traduisant MMode	herbelin	2004-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5361 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5360 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5359 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
\| \| \| \| \| \| \| \| \|	- fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug coercions imbriquees + suppression des coercions avant filtrage sur ↵	herbelin	2004-02-18
\| \| \| \| \| \|	notations pour respecter le cpmt v7 et la symtrie avec le parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5357 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5356 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de lconstr, constr et binder_constr dans Print Grammar constr	herbelin	2004-02-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5354 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5353 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Erreur dépendance en Util lui-même	herbelin	2004-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5351 85f007b7-540e-0410-9357-904b9bb8a0f7
*	accomodate the .. extension	bertot	2004-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5350 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adds a new command for searching a pattern inside the premises of theorems	bertot	2004-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5349 85f007b7-540e-0410-9357-904b9bb8a0f7
*	corrects a bug in name reservation, simplifies or_intro, removes dead code	bertot	2004-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5348 85f007b7-540e-0410-9357-904b9bb8a0f7
*	export the general function for getting information from the environment	bertot	2004-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5347 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5346 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5345 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5344 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement array_map_left and co dans Util	herbelin	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5343 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout array_map_left and co	herbelin	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5342 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation du comportement de Notation et Reserved Notation	herbelin	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5341 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et ↵	herbelin	2004-02-13
\| \| \| \| \| \|	Reserved Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petit bug avec Extraction Optimize	letouzey	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5339 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug numerotation des occurrences pour 'simpl id at n' (suite)	herbelin	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5338 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adds a new command add_rec_path for the parser program and changes add_path	bertot	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug numerotation des occurrences pour 'simpl id at n' (2 protections ↵	herbelin	2004-02-13
\| \| \| \| \| \|	maintenant !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5336 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adds the possibility to have terms (and not just identifiers) as hints	bertot	2004-02-13
\| \| \| \| \| \| \|	Adds the 'Reserved Notation' command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5335 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adds the possibility to have terms (and not just identifiers) as hints	bertot	2004-02-13
\| \| \| \| \| \| \|	Adds the 'Reserved Notation' command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5333 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5332 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5331 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus d'explicitation d'un message d'erreur	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5330 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation erreur interp_notation	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5329 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
\| \| \| \| \| \| \| \|	dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
\| \| \| \| \| \| \| \|	dans le module de leur définition. Correction bug de nommage de la notation en présence de "{ _ }" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5327 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
\| \| \| \| \| \| \| \|	dans le module de leur définition. Internalisation des preident comme des noms qui ne sont pas des références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5326 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mauvaise dependance en states7/initial.coq	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5325 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation erreur interp_notation	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5324 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug affichage en presence de '{ _ }'	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lazy was translated to cbv, obviously wrong	bertot	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5322 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout delimiteur pour bool_scope	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5320 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
\| \| \| \| \| \| \| \| \| \| \|	notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A{B}+{C}" en présence d'une notation "_ { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A\|P}" etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implicits can have an optional list of argument, which is different	bertot	2004-02-12
\| \| \| \| \| \| \| \| \|	from an empty list of arguments. in H at 2 \|- * was badly translated in clauses (for replacement tactics) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5318 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5317 85f007b7-540e-0410-9357-904b9bb8a0f7
*	a new version that uses intro patterns, but the code still needs some cleaning	bertot	2004-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5316 85f007b7-540e-0410-9357-904b9bb8a0f7
*	removes a lot comments that may be useful for later code maintenance, but	bertot	2004-02-11
\| \| \| \| \| \| \|	should not be kept in the sources because they only contain obsolete code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5315 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5314 85f007b7-540e-0410-9357-904b9bb8a0f7