index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
reduction.ml
Commit message (
Expand
)
Author
Age
...
*
reduction des let in dans whd_programs
filliatr
2001-04-23
*
réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...
filliatr
2001-04-11
*
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-10
*
amelioration de la structure des univers
barras
2001-03-28
*
amelioration de la consommation memoire de la conversion en eta-expansant
barras
2001-03-23
*
entetes
filliatr
2001-03-15
*
nouvelle implantation de la reduction
barras
2001-03-01
*
retire profile
mohring
2001-02-28
*
Changement de subst_meta
mohring
2001-02-28
*
Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...
herbelin
2000-12-26
*
Bug mauvais environnement dans le test d'eta-conversion
herbelin
2000-12-20
*
Ajout map_constr_with_full_binders et strong pour Simpl
herbelin
2000-11-27
*
deplacement poly_args; iterateurs sur les segments
filliatr
2000-11-22
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...
herbelin
2000-10-26
*
Bug réduction suite modifs let-in
herbelin
2000-10-24
*
Simplifications/questions
herbelin
2000-10-23
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Idem pour défs locales dans Var
herbelin
2000-10-11
*
Delta des défs locales en de Bruijn toujours pas stable
herbelin
2000-10-11
*
Bug splay_prod_assum
herbelin
2000-10-06
*
Mise en conformité nouveau Simpl pour Fix
herbelin
2000-10-04
*
Touche finale à la réduction du let in dans conv et closure
herbelin
2000-10-04
*
Renommage AppL en App
herbelin
2000-10-01
*
Code comateux
herbelin
2000-10-01
*
Retrait de whd_ise1_metas
herbelin
2000-09-26
*
On laisse les LetIn dans les types des constructeurs et des éliminations
herbelin
2000-09-15
*
Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...
herbelin
2000-09-14
*
Vers la paramétrisation des fonctions de Reduction et vers la fusion de
herbelin
2000-09-12
*
Correction pour make doc
herbelin
2000-09-10
*
Suppression de Abst
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Retrait de decomp_prod non conforme à sa spec
herbelin
2000-06-02
*
Bug DLAM dans strong
herbelin
2000-06-02
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Nettoyage de Generic
herbelin
2000-05-31
*
Bug existential_value au lieu de existential_type + divers sur existential
herbelin
2000-05-25
*
suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls
herbelin
2000-05-22
*
Suite restructuration inductifs; changement nom module Constant en Declarations
herbelin
2000-05-22
*
Restructuration des outils pour les inductifs.
herbelin
2000-05-18
*
Ajout d'un strong 'light'
herbelin
2000-05-05
*
Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)
herbelin
2000-05-04
*
Retrait fullmind de inductive_summary pour simplicité
herbelin
2000-04-27
*
Abstraction du type typed_type (un pas vers les jugements 2 niveaux)
herbelin
2000-04-20
*
Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sort...
herbelin
2000-03-21
*
Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'
herbelin
2000-03-17
*
Ajout du test d'égalité des vecteurs dans convert_forall2.
herbelin
2000-03-08
*
Nouveaux types 'constructor' et 'inductive' dans Term;
herbelin
1999-12-15
[prev]
[next]