aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2003-05-26GIntuition now matches Intuition up to hyps renaming.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4080 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26Added breakpoint in Ground tactic.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4079 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26moved engine.ml4 to ground.ml4, added option 'Ground Depth'corbinea
fixed utf8.vo dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4078 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-25Ground and CCsolve updatescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4055 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notations ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4053 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4052 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4051 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4044 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-16Major Ground tactic update, sensible performance improvementcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4026 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Notations arithmetiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4008 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-08bugfixes in Ground.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3997 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07Enhancement of the Ground tactic, addition of GTauto and GIntuition.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28bug concernant les projecteurs de Record avec args logiquesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3967 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28adaptation a Acc_iterletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3965 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-26bugfix in Ground tacticcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3957 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-25Added the Ground tactic.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3943 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Ajout "at next level" dans Notationherbelin
Mise en place structure pour définir un objet en même temps que sa notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3938 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Ooopsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3937 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17temporaireletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3935 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16BIG MAJ Extraction:letouzey
------------------ - (Recursive) Extraction Module devient (Recursive) Extraction Library (pour cause d'ambiguite avec les nouveaux modules Coq). - un nouveau Extraction Module qui extrait dans le toplevel tout module Coq - tout fixpoint est de nouveau inlinable (Yves). - fix bug du calcul d'env minimal des modules en extraction monolithique. - un nouveau fichier Modutil regroupant manques de Modops & functions specifiques aux modules MiniML - plus d'aliases a trainer (mais des substitutions des le depart) - ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes et les functors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3915 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-11Explicitation arguments de eqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3914 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Alignement du comportement des implicites d'inductif en sortie de section ↵herbelin
sur celui des constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3880 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3875 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Mauvaise resolution conflit dans commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3859 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-03Légères simplifications code de Field; message d'erreur si pas égalitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3841 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01remplace == par = dans la tactique field pour que le debugger marche a ↵narboux
nouveau apres suppression de == par hugo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3837 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Fail 1 pour traverser le matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3832 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Noms absolusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3829 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Plus de eqT; message Failherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3826 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
lambda-abstraction inside a Cases. I had to make the term of the induction principle a bit less clean (more eta expansions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3817 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31minus a changé d'emplacement -> omega pas contentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3814 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-25Extract Constant marche avec les axiomes schémas de typesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3788 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-24Bugfix pour Linear.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3785 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21Fin de la résurrection de Linear.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3781 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12* Ajout du traducteur nouvelle syntaxe *barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3760 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 03:46:48 +0000