aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
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@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2721 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@2720 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@2719 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Pour les tactiques dépendant de Falseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2718 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Implante la macro camlp4 VERNAC COMMAND EXTENDherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2717 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Implante la macro camlp4 TACTIC EXTENDherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2716 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichier des expressions de commandes vernaculairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2715 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichier des expressions de tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2714 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29MAJ 7.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2713 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2712 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-27Ajout de Eval, Inst et Checkdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-27Changement Filename.is_relative en Filename.is_implicit, plus pertinentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2710 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-22Oublisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2707 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-22*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2706 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-22*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2705 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-22Correction of a bug in Intuition (no more decomposition of dependent pairs).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2704 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-21Field + MapleModedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2703 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2702 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16ARCH passe de Makefile à config.distribherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2701 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2700 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16MAJ V7.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2699 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16Ajout Peano_dec et Compare_decherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2698 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16suppression de inf_decidable dans ZArith_dec (pour SeachPattern)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2697 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
gauche à droite des hypothèses dans Intuition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2696 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
gauche à droite des hypothèses dans Intuition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2695 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2694 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
VTactic utilisé pour les fermetures de ltac s'appelle maintenant VTacticClos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2693 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusbarras
(did not return an ordered list of monomials). - improved unary negation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2692 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Contournement de la fermeture ML dans VContextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2691 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2690 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15MAJ V7.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2689 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2688 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15mention -dump-globfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2687 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2686 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
- Protection des "Match Context" contre les exceptions non UserError ni Fail - Remplacement des fermetures ML dans VTactic et VFTactic par des expressions de tactiques pour permettre l'intégration de Tactic Definition dans les états - Changement en conséquence de Tauto git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2685 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14Utilisation d'une construction spéciale SECVAR pour gérer laherbelin
globalisation des variables de section (en espérant plus de robustesse vis à vis des bugs récurrents de Infix pour les variables avec implicites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2684 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14petite erreur de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2683 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14modification de clenv_merge:barras
on ajoute en premier lieu les contraintes concernant le terme puis apres celles concernant le type de chaque instantiation, au lieu d'alterner l'ajout de contraintes de terme et de type. A l'essai. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2682 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14Ajout de la modification des sortes d'eliminationmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2681 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14Changement de eq en eqT comme equivalence de setoide par defaut.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2679 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14encore des lemmes sur Zdivfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2678 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2677 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:20:47 +0000