aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2002-04-24petit bug dans les noms de fichiersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2662 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique ↵filliatr
FourierR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2659 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-18*** empty log message ***letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2657 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17jLogic.mli remplace par jolic.mliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2652 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2651 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-15Refine the procedure that generalizes context to current goal.huang
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2646 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-15maj doc extraction dans repertoire contrib/extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2643 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12maj test des realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2636 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12petit bug avec dummy_lamsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2635 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2632 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08extraction.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2623 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08babioles de renommagesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2622 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ↵letouzey
dummy git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2619 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08export de la fonction Reductionops.find_conclusion pour l'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2617 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-05Suppression de l'application de f_equal2 pour "mult" (non inversible);herbelin
Application de f_equal2 pour "plus" seulement si soit les membres droits soit les membres gauches sont égaux. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2616 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-05mise jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2613 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04*** empty log message ***huang
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2608 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04Add citationshuang
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2607 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-28reparation du cas des arguments de type qui sont des arités + patch dummy ↵letouzey
applied git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2574 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-27Simplification de Proof_type.prim_ruleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-26Refonte complete de la génération des types MLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2568 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-22An intuitionistic first-order theorem prover -- JProver.huang
See the "README" file for more information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21reparation du test des realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2561 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21considerations de pretty-printletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2558 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21deux fichiers supplementaires de customisation d'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2557 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21changement du test extraction suite aux modif ininingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2556 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 19:58:35 +0000