aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Ajout EVALGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | 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
* Réorganisation des tclTHEN (cf dev/changements.txt)Gravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fichiers tactics/*.ml4 remplacent les tactics/*.vGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour les tactiques dépendant de FalseGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implante la macro camlp4 VERNAC COMMAND EXTENDGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implante la macro camlp4 TACTIC EXTENDGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fichier des expressions de commandes vernaculairesGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fichier des expressions de tactiquesGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2714 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ 7.3Gravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Eval, Inst et CheckGravatar delahaye2002-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement Filename.is_relative en Filename.is_implicit, plus pertinentGravatar herbelin2002-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2710 85f007b7-540e-0410-9357-904b9bb8a0f7
* OublisGravatar herbelin2002-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2707 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2706 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of a bug in Intuition (no more decomposition of dependent pairs).Gravatar corbinea2002-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Field + MapleModeGravatar delahaye2002-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2703 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2702 85f007b7-540e-0410-9357-904b9bb8a0f7
* ARCH passe de Makefile à config.distribGravatar herbelin2002-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2701 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2700 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ V7.3Gravatar herbelin2002-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Peano_dec et Compare_decGravatar herbelin2002-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2698 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de inf_decidable dans ZArith_dec (pour SeachPattern)Gravatar filliatr2002-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2697 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deGravatar herbelin2002-05-15
| | | | | | | 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
* Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deGravatar herbelin2002-05-15
| | | | | | | 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
* MAJGravatar herbelin2002-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement VTactic est gardé pour y plonger les tactiques ML, leGravatar herbelin2002-05-15
| | | | | | | 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
* - abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusGravatar barras2002-05-15
| | | | | | | | (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
* Contournement de la fermeture ML dans VContextGravatar herbelin2002-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2691 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2690 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ V7.3Gravatar herbelin2002-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2689 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2688 85f007b7-540e-0410-9357-904b9bb8a0f7
* mention -dump-globGravatar filliatr2002-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2687 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2686 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Changement de l'ordre de filtrage dans "Match Context"Gravatar herbelin2002-05-14
| | | | | | | | | | | - 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
* Utilisation d'une construction spéciale SECVAR pour gérer laGravatar herbelin2002-05-14
| | | | | | | | | 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
* petite erreur de syntaxeGravatar barras2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2683 85f007b7-540e-0410-9357-904b9bb8a0f7
* modification de clenv_merge:Gravatar barras2002-05-14
| | | | | | | | | 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
* Ajout de la modification des sortes d'eliminationGravatar mohring2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2681 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout des theoremes eqT_rec_r et eqT_rect_r pour RewriteGravatar barras2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de eq en eqT comme equivalence de setoide par defaut.Gravatar clrenard2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2679 85f007b7-540e-0410-9357-904b9bb8a0f7
* encore des lemmes sur ZdivGravatar filliatr2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2678 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveaux lemmes dans Zdiv (Claude Marche)Gravatar filliatr2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation des de Bruijn pour la constructions des records et de leur ↵Gravatar herbelin2002-05-13
| | | | | | projections; plus de projection si le nom est '_' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas de projection si le nom d'un champ est '_' dans un RecordGravatar herbelin2002-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de souplesse pour les constructeurs encapsulés sous des définitionsGravatar herbelin2002-05-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2674 85f007b7-540e-0410-9357-904b9bb8a0f7
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2672 85f007b7-540e-0410-9357-904b9bb8a0f7
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2671 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 02:28:48 +0000