aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-06-03Factorisation de 'Show Programs' au premier niveau de Vernac_.commandherbelin
2002-05-31Les VContext ne sont plus des fermetures (temporaire)delahaye
2002-05-31Ajout d'occurrences de Field (ne pas enlever)delahaye
2002-05-31.depend.coq remis a jourletouzey
2002-05-30Ajout des -I contribherbelin
2002-05-30Nettoyageherbelin
2002-05-30Mise au point de declare_red_exprherbelin
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29syntax/PPTactic.v passe au niveau MLherbelin
2002-05-29Déplacement de proofs vers tacticsherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Introduction de syntaxe convivial +,*,<=,<,>=herbelin
2002-05-29Double Induction prend maintenant des noms d'hyppthèsesherbelin
2002-05-29Utilisation d'Infix/Distfix autant que possibleherbelin
2002-05-29Contournement des My_special_variableherbelin
2002-05-29*** empty log message ***herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Ajout EVALherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Pour les tactiques dépendant de Falseherbelin
2002-05-29Implante la macro camlp4 VERNAC COMMAND EXTENDherbelin
2002-05-29Implante la macro camlp4 TACTIC EXTENDherbelin
2002-05-29Fichier des expressions de commandes vernaculairesherbelin
2002-05-29Fichier des expressions de tactiquesherbelin
2002-05-29MAJ 7.3herbelin
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
2002-05-27Ajout de Eval, Inst et Checkdelahaye
2002-05-27Changement Filename.is_relative en Filename.is_implicit, plus pertinentherbelin
2002-05-22Oublisherbelin
2002-05-22*** empty log message ***desmettr
2002-05-22*** empty log message ***herbelin
2002-05-22Correction of a bug in Intuition (no more decomposition of dependent pairs).corbinea
2002-05-21Field + MapleModedelahaye
2002-05-16MAJherbelin
2002-05-16ARCH passe de Makefile à config.distribherbelin
2002-05-16MAJherbelin
2002-05-16MAJ V7.3herbelin
2002-05-16Ajout Peano_dec et Compare_decherbelin
2002-05-16suppression de inf_decidable dans ZArith_dec (pour SeachPattern)filliatr
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
2002-05-15MAJherbelin
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
2002-05-15- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:43:27 +0000