aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Extension de la primitive ltac fresh pour qu'elle accepte une liste deGravatar herbelin2006-10-24
* bug #1194: normalisation evars a la sortie de focusGravatar barras2006-10-23
* affichage des ... dans les scriptsGravatar barras2006-10-16
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* improve the amount of information given by the Ltac tactic debuggerGravatar bertot2006-08-28
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Protection mode Debug On contre Ctrl-DGravatar herbelin2006-05-05
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* replacing whd_betaiotaevar_preserving_vm_cast Gravatar jforest2006-04-14
* patch pour contourner l'échec de type_of_applied_inductive sur un inductif a...Gravatar herbelin2006-04-11
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Patch envoy\'e par Benjamin Gregoire, permettant de corrigerGravatar letouzey2006-03-24
* 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
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* 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
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* changement d'egalite pour le named_context_valGravatar gregoire2005-12-05
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Confusion assert/error détectée par nouveau warning X de ocaml 3.09Gravatar herbelin2005-11-04
* catchable_exception laisse passer les InductiveErrorGravatar werner2005-10-27
* Correction double bug #986: Fold ne préserve pas nécessairement le typage e...Gravatar herbelin2005-07-13
* unification: evar_define checks the free variables are bound in the evar contextGravatar barras2005-05-28
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Allow auto to have a parametric argument (wish #967)Gravatar herbelin2005-05-15
* Protection against saving a proof with still non-instantiated evars (cf bug #...Gravatar herbelin2005-04-29
* Protection against saving a proof with still non-instantiated evars (cf bug #...Gravatar herbelin2005-04-29
* Implementation of a new backtracking system, that allow to go backGravatar coq2005-04-20