aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-06-06Ajout exemple Yves renommage différent d'une var de sectionherbelin
2002-06-05affaiblissement hyp de Zmult_reg_leftfilliatr
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...herbelin
2002-06-05Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotificationherbelin
2002-06-05Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructherbelin
2002-06-05Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...herbelin
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
2002-06-04*** empty log message ***courant
2002-06-04'make check' echoue si au moins un test echoue.courant
2002-06-03*** empty log message ***herbelin
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et re...herbelin
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:09:21 +0000