aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
* Correction erreur grossière de non restauration d'état en cas de retour exc...Gravatar herbelin2005-03-19
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...Gravatar herbelin2004-12-31
* Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...Gravatar herbelin2004-12-31
* Code mortGravatar herbelin2004-11-18
* Mise en pageGravatar herbelin2004-11-17
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* simplification de clenvGravatar barras2004-09-10
* When refining a given term, the primitive refiner used to accepts some casts,Gravatar sacerdot2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* deplacement de clenv vers pretypingGravatar barras2004-09-03