aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2002-03-20Intuition now takes an (optional) tactic as parameter. This tactic iscourant
used to solve the goal remaining after propositional destructuration of the goal and the hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2554 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19Exportation de SplitRmult et SplitAbsoludelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2541 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-17Field ne fait maintenant que les reductions necessairesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2539 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-13Ajout de lemmesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2530 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-07*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2520 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05petits changements afin de profiter du nouveau Rewrite/inbarras
(l'unification marche mieux) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2512 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Ajout andb_true_eq pour PolyList.list_beqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2497 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22Doc + ajout fold_symmetric et nth_Inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2493 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22Docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2492 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-21code mort dans tactinterp; plus de Debug On/Off dans Correctnessfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2490 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19Uniformisation des theoremes dans Set et Type (def. de Acc_rect etbarras
well_founded_induction_type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2485 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14Syntaxe IF then else au lieu de either and_then or_elsebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2473 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31changement generation de schema d'elimination, False_rec est primitif, ↵mohring
Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-29modification de la definition des def inductives unitaires et autorisation ↵mohring
d'elimination sur la sorte Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2442 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25Bug affichage de O (de nat) dans une expression sur Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2439 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25Zdiv et Zmod dans Zcomplementsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2437 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Bug commentaire (*i i*)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2415 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18amadouage de coqwebletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2413 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de ↵letouzey
contrib/omega vers theories/ZArith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2406 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-10Modifs incongrues dans le précédent commitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2385 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-09MAJ des Id pour coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2384 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-07Ajout en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2381 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Passage coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2371 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Commentaire coqweb non ferméherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2370 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Extension de Even et Div2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2367 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2343 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-07*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2280 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-07*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2279 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Amélioration nommage hypothèses NewInduction (et incompatibilités)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2274 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2273 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2272 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2270 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2269 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2268 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2267 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-04Traitement t de -1<>0delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2265 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-04Backtrack sur le commit du 30.11.2001delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2263 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-03*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2262 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2260 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2259 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2258 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30Ajout du fichierdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2257 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30Modification de Reals pour integrer les modificationsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2255 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30Ajout du fichier concernant le carre et la racine carreedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2254 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30Integration de nouveaux lemmesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2253 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2252 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30Intégration de nouveaux lemmes.desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2251 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-02 02:56:42 +0000