aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2002-03-21modification de l'auto-inliningletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2555 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-20renversement du renommage des variablesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2552 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-20reparation du controle de l'apparition des termesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2551 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-20reorganisation des simplifications: letin eta-expansé apres le kill-dummyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2550 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-20un peu moins d'eta-expansion autour des Globletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2549 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19bug optimize_fix fait trop totletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2548 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19suite bug Dglob constantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2547 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19bug avec les MLglob vraiment constantsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2546 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19travail sur les stratégies de réductionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2545 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19remplacement des deux constants prop/arity par une seule dummy + ↵letouzey
pretty-print des fix mutuels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2544 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19Fix d'un bug sur le test des inversesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2542 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
Field term (nouveau) Injections dans l'interpreteur de tactiques Exportation de quelques entrees de grammaires Exportation de quelques fonctionnalites des definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-15epsilonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2537 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-15un peu de mise a jour de la doc extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2535 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-15evite les clash avec le type ocaml unitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2534 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-15gros commit: principalement ajout des lambdas arity + leur optimisation en ↵letouzey
temps normal + beaucoup de simplifications diverses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2532 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-14reparation semi setoid ringclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2531 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-11Factorisation de la grammaire pour Extraction Language.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2522 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-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-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-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-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-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-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-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-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-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
2002-02-08affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien ↵filliatr
faire si pas debug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2462 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07petit nettoyage de kernel/inductivebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07un assert false de trop (MLexn peut avoir des args)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2458 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-06oubliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2457 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-06gros changement dans mlutil.ml: ajout d'une elimination globale des propletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2456 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-05Ajout d'optimisations locales kill_propletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2452 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31adaptation de l'extraction aux changements de Christine concernant rec/rect ↵letouzey
et False_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2448 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31extraction des CoInductives via les Lazy d'ocamlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2446 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25patch Omega (bug 129)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2436 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-23In Pcoq, the search commands had an erroneous behavior. Bound variablesbertot
in theorems were renamed to avoid the names present in the current goal's context. This version corrects this problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2425 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-21Correction de Pierre Crégut pour le bug MERGE_EQherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2421 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-21Zinv -> Zoppfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2419 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Bug MERGE_EQherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2416 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Plusieurs arguments autorisés pour Require et Read Moduleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2412 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 00:56:14 +0000