aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-26 14:28:31 +0000