aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Correction bug #1519Gravatar herbelin2007-04-28
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...Gravatar notin2007-04-26
* fin des conclusions multiplesGravatar corbinea2007-04-26
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
* Extension to the general sequence operator (tactical). Now in addition to ...Gravatar emakarov2007-04-02
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Report de révision 9583 de la v8.1 dans le trunkGravatar notin2007-02-01
* Suppression de code mortGravatar notin2007-02-01
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
* "suffices" implemented + syntax cleanupGravatar corbinea2007-01-28
* decl mode: anonymous factsGravatar corbinea2007-01-25
* Correction du bug #1315:Gravatar notin2007-01-22
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
* 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