aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface
Commit message (Expand)AuthorAge
* Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.Gravatar msozeau2007-01-29
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Extension de fresh (suite)Gravatar herbelin2006-10-24
* affichage des ... dans les scriptsGravatar barras2006-10-16
* Notations:Gravatar herbelin2006-10-09
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Suite commit 9110 (uniformisation position notation dans les blocs inductifs)Gravatar herbelin2006-09-01
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
* making otags working Gravatar jforest2006-08-22
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Suite remplacement VernacDebug par VernacSetOptionGravatar herbelin2006-07-06
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
* Suite passage ident -> hyp dans syntaxe de 'replace with in'Gravatar herbelin2006-06-23
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Détection bug rawwit suitecorrection trou de typage create_argGravatar herbelin2006-06-08
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...Gravatar herbelin2006-01-21
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* remove warnings that were left in the directory contrib/interfaceGravatar bertot2006-01-11
* removes several warnings in contrib/interfaceGravatar bertot2006-01-11
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...Gravatar herbelin2005-12-30
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* Changement des named_contextGravatar gregoire2005-12-02
* adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,Gravatar bertot2005-11-14
* Types inductifs parametriquesGravatar mohring2005-11-02
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20