aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-03-07Simplify_eq echouait sur des hypotheses trivial comme O=Obarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2518 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-07Clear ne substitue plus le corps dans le reste du butbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2517 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2516 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05ajout d'une entree 'binaries' pour recompiler coq mais pas les theoriesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2515 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05cas des constructeurs singletons. Messages d'erreur. Revision de ↵letouzey
test_extraction.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2514 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05assert failure avec Conditional Rewritebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2513 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-05unification faite de gauche a droite (et non pas l'inverse) pour eviter quebarras
clenv_typed_unify plante trop facilement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2511 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05suppression de code mortbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2510 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2509 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Big commit extraction:letouzey
- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell) - Retour des inductifs singletons et vides dans extraction.ml (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type) - maintenant par defaut Recursive Extraction === Extraction "file" - kill_prop global est fait dans extraction.ml selon typage (a suivre...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 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-03-01Nouveau comportement: Delta ne s'applique pas aux variables liées par un letherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2506 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-01Prise en compte des corps de letin dans les hypothèsesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2505 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-01labels appliques dans un ordre incorrectbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2504 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-01convert_hyp a change de typebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2503 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Uniformisation convert_hypherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2502 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Uniformisation convert_hyp; correction problème de dépendance dans letin_tacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2501 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2500 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28ajout option_compareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2499 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Generalisation de l'utilisation de l'unification d'ordre 2barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2498 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-27modifs des preambules d'extraction modulaireletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2496 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-27-dump-glob dans le usagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2495 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-25pretty print des Cases devenant des let-inletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2494 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-22suppression de pop_namedbarras
meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 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-20Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parceddr
qu'il entre en conflit avec le module Errors ajouté dans OCaml courant (future version OCaml 3.05). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2489 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19typage du produit: type_judgment appele avec contexte incorrectbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2488 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19meilleur message d'erreur lorsqu'on type une evar qui n'existe pasbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2487 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19Le type des evars transformees en meta n'etait pas normalise, et des Evarsbarras
definies y apparaissait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2486 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-19Elim dependente n'appelait pas la bonne fonction pour calculer le predicatbarras
d'elimination (d'ou le bug avec Dependent Inversion) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2484 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-18bug #134: on appelait solve_simple_eqn avec une evar qui etait resoluebarras
par comparaison de ses arguments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2483 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-18but de CutRewrite <- (assert false)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2482 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15suite et fin (?) de haskell: gestion des modules, mise en place du'un testletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2480 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15bootstrap consistent avec les options de la ligne de commandefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2478 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15debut de gestion des open pour extraction modulaireletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2477 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14qq inline manuels (sigS_rec ...) + utilisation de library_partletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2476 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 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-02-12Raffinement library_partherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2472 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12petite modif pour ne pas expanser trop de let pendant l'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2471 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12suppression de la condition de la permutation case/funletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2470 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12pretty printletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2469 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12Test & correction de la production de code Haskellletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2468 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:06:17 +0000