index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Orthographe de 'instantiate'
herbelin
2005-12-17
*
changement d'egalite pour le named_context_val
gregoire
2005-12-05
*
Changement des named_context
gregoire
2005-12-02
*
parametres inductifs
mohring
2005-11-28
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
Correction bug invert_names (cf bug #1031)
herbelin
2005-11-02
*
Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...
herbelin
2005-09-09
*
Un vieux bug d'affichage des lieurs (cf bug #1005)
herbelin
2005-09-06
*
pas besoin de List.length pour savoir si une liste est vide
letouzey
2005-08-19
*
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
letouzey
2005-08-19
*
backtrack sur le typage des instantiations d\'evars
barras
2005-06-09
*
evar declarees avec mauvais type
barras
2005-06-08
*
pas de filtrages partiels
barras
2005-06-07
*
reparations de quelques petits bugs d\'unification + introduction de la notio...
barras
2005-06-07
*
essai de typage des instantiations d\'evars
barras
2005-06-06
*
eradication de Evarutil.w_Define
barras
2005-06-05
*
assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...
barras
2005-06-05
*
unification: evar_define checks the free variables are bound in the evar context
barras
2005-05-28
*
Added subtac contrib.
coq
2005-05-25
*
Added clenv_environments_evars that behaves as clen_environments but
sacerdot
2005-05-24
*
WARNING: unification changed (to fix a bug).
sacerdot
2005-05-24
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Documentation
herbelin
2005-05-20
*
A wish by Bas Spitters granted: a little more of unification up to
sacerdot
2005-05-19
*
Fix bug in prepare_predicate_from_tycon; improved error message when no claus...
herbelin
2005-04-29
*
Backtrack sur la substitution combinée avec l'instanciation en réponse à l...
herbelin
2005-03-15
*
Backtrack version 1.82 awaiting for better understanding of the consequences ...
herbelin
2005-03-12
*
Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...
herbelin
2005-03-11
*
A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...
herbelin
2005-03-10
*
A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...
herbelin
2005-03-10
*
bug #931 (continued): no recursion on the evars instantiation
herbelin
2005-03-09
*
Fix bug #931: leave dependent evars as such for refine
herbelin
2005-03-08
*
Ajout fold
herbelin
2005-03-08
*
Code mort
herbelin
2005-03-01
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Moving subst_inductive from tacinterp to inductiveops for better for reuse in...
herbelin
2005-02-18
*
Ajout it_mkNamedProd_wo_LetIn
herbelin
2005-02-18
*
Ajout splay_lambda
herbelin
2005-02-18
*
Uniformisation de destApplication en destApp
herbelin
2005-02-12
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
Correction de la précédence des contexts de variables rel, ltac et var
herbelin
2005-02-02
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
HUGE COMMIT
sacerdot
2005-01-03
[next]