aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-03-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5400 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Exemple de Fredericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5399 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Expansion du type par nécessité dans le cas d'affichage d'implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5398 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28MAJ Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5397 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Traduction 'Cases' en pattern-matchingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5396 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Eviter la stricte redondance de regles de grammaires v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5395 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Prise en compte des implicites au travers des notations et abbreviationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5394 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5393 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5392 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27Erreur de Bruijn et oubli substitution alias dans annotation du 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5391 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27Ajout test synthese du predicat a partir du cast d'un filtrage avec dependancesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5390 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27*** empty log message ***filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5389 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5388 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26added breakpoints to help idecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5387 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Keep structure information for Fixpoint declaration and Fix termsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Not all cases for coercions and locality were handledbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5385 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Inclusion des annotations de type des filtrages dans 'Set Printing All'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5384 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5383 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-25indexation Record / bug gallina sur := en V8filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5382 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5381 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5380 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-24coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5379 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-24*** empty log message ***filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5378 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-24coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5377 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5376 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-23Generating of annotations added to Makefile.dircoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5375 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-23corrects the treatement of SubClass declarationsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5372 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-21Correction oubli de report d'une modification de g_vernac (1.69) vers ↵herbelin
g_vernacnew git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5371 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5370 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-21Export des arguments scope au chargement, pas a l'ouverture (2eme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5369 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5368 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-20Export des arguments scope au chargement, pas a l'ouvertureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5367 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-20commit précédent erronéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5366 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5365 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5364 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-19makes sure the following examples are well-treated:bertot
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
2004-02-19files from contrib/interface need files from contrib/field, the variablebertot
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
2004-02-19Bugs/insuffisances trouvees en traduisant MModeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5361 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5360 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5359 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
- 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
2004-02-18Bug coercions imbriquees + suppression des coercions avant filtrage sur ↵herbelin
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
2004-02-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5356 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-17Ajout de lconstr, constr et binder_constr dans Print Grammar constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5354 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5353 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16Erreur dépendance en Util lui-mêmeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5351 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16accomodate the .. extensionbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5350 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16adds a new command for searching a pattern inside the premises of theoremsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5349 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16corrects a bug in name reservation, simplifies or_intro, removes dead codebertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5348 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 16:05:58 +0000