aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-04-07lconstr pour genterm en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3864 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Ajout translateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3863 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3862 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Nommage explicite des hypotheses introduites quand le nom existe aussi comme ↵herbelin
global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3861 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3860 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-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@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Stratégie d'affichage des coercions plus défensive (mais pas très optimale)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3856 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3855 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3854 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Espaces superflusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3853 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Renommage unicite/unicity pour la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Aérer les := et : de "assert"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3851 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Ajout cas Matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3850 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07BEST redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3849 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Suppression des explicitations d'implicite inutilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3848 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun impliciteherbelin
ne s'insére pour les références dont tous les arguments sont implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3847 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Options d'affichage maintenant dans Constrexternherbelin
Ajout "Set/Unset Printing Implicits" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3846 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Options d'affichage maintenant dans Constrexternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3845 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3844 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-03Documentation, généralisation à eq sur Type, preuves d'équivalence desherbelin
4 axiomes (K, UIP, eq_rec_eq, eq_dep_eq) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3843 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-03Backtrack du commit de Christine, qui posait probleme avec FTCletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3842 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-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3840 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-02espace manquantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3839 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-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3836 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Déplacement with_option dans Optionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3835 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Correction bug #261 + amélioration nommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3834 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Extension de Replace aux égalités entre preuvesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3833 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-04-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3831 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3830 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-31Ajout double_plusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3828 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout Implicit Variable Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3827 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-31Ajout d'un message à FailTac; localisation des appels à des tactiques ↵herbelin
définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un choix 'onlyparse'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3822 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Suppression des alias eqT/exT/exT2 en nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3821 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout VernacReserve et suppression des types re-inferablesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Restauration de make_all_different (disparu depuis version 1.74) car sinon ↵herbelin
detype echoue sur les variables anonymes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3819 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Bug pattern_occ_hyp_listherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3818 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-31Notation eqT superflueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:51:09 +0000