aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-06-11Tests pour la tactique Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2777 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2776 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2775 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11Ranalysis.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2774 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07L'ordre supérieur avait quelque peu été oublié dans l'unification...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2772 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07extraction vers schemeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07Adding file theories/ZArith/Zsqrt.v that contains a square root function.bertot
actually three functions are provided, one working on positive numbers (it is structurally recursive), one with a strong specification (Zsqrt), and one with a weak specification (Zsqrt_plain). For the function with a weak specification an extra theorem is also provided. The decision functions in ZArith_dec have been made transparent so that computation with the square root function also becomes possible with Lazy Beta Iota Delta Zeta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07Ajout de FNL ou utilisation de msgnlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2769 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07Locate n'échoue plus: déplacement de Remark1 et Remark2 dans outputherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2768 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07I added a comment on the tactic compute_POS.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2767 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07This example does not work in coq-7.3, but does in coq-7.2.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2766 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout coercion constr vers hyp quantifiéeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2765 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout exemple JCF conflit variable interne, variable de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2764 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Tentative de réparation d'un bug Omega: une variable de section qui après ↵herbelin
effacement ne peut être renommée pareille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2763 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Des exemples sérieuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2762 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs ↵herbelin
de Z et R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2760 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout exemple Yves renommage différent d'une var de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2759 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05affaiblissement hyp de Zmult_reg_leftfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2758 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans ↵herbelin
Simplify_eq et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2757 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2756 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2755 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq ↵herbelin
et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2754 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; ↵herbelin
rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2753 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-04*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2752 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-04'make check' echoue si au moins un test echoue.courant
Les distributions binaires ne peuvent etre faites que si 'make check' reussit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2751 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2750 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et ↵herbelin
retouche des Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2746 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Factorisation de 'Show Programs' au premier niveau de Vernac_.commandherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2744 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-31Les VContext ne sont plus des fermetures (temporaire)delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2743 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-31Ajout d'occurrences de Field (ne pas enlever)delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2742 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-31.depend.coq remis a jourletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2739 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Ajout des -I contribherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2738 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2737 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Mise au point de declare_red_exprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2736 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29syntax/PPTactic.v passe au niveau MLherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2733 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Déplacement de proofs vers tacticsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2732 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2731 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Introduction de syntaxe convivial +,*,<=,<,>=herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2730 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Double Induction prend maintenant des noms d'hyppthèsesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2729 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Utilisation d'Infix/Distfix autant que possibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2728 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Contournement des My_special_variableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2727 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2726 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2725 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2724 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Ajout EVALherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2723 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 00:32:43 +0000