index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
term.ml
Commit message (
Expand
)
Author
Age
*
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...
herbelin
2001-09-19
*
Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...
herbelin
2001-09-09
*
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
*
Ajout hashconsing univers
herbelin
2001-07-03
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
Ajout d'une fonction de remplacement d'un sous-terme par un terme.
clrenard
2001-05-15
*
Changement de la structure des points fixes
barras
2001-05-03
*
interdiction occ positives ET negatives dans Pattern
werner
2001-04-24
*
Suppression de mk_constr qui ne respectait pas l'invariant des applications (...
herbelin
2001-04-15
*
entetes
filliatr
2001-03-15
*
compare_constr independent du groupement des applications.
barras
2001-03-08
*
Re-Déplacement extended_rel_list
herbelin
2001-03-05
*
nouvelle implantation de la reduction
barras
2001-03-01
*
Changement de subst_meta
mohring
2001-02-28
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Ajout global_vars_decl
herbelin
2001-01-24
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Ajout map_constr_with_full_binders et strong pour Simpl
herbelin
2000-11-27
*
Reparation IsMutConstruct + Transparent
mohring
2000-11-23
*
Introduction constant_path = section_path
herbelin
2000-11-20
*
Code mort
herbelin
2000-11-10
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Nouveau type rec_declaration
herbelin
2000-10-11
*
Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)
herbelin
2000-10-11
*
correction bug univers (dummy_univ)
filliatr
2000-10-06
*
Rebranchement de la tactique Let
herbelin
2000-10-03
*
Renommage AppL en App
herbelin
2000-10-01
*
Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...
herbelin
2000-10-01
*
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-12
*
Suppression de Abst
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Pattern matching de sous-termes
delahaye
2000-08-17
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Ajout fonctions sur les arités
herbelin
2000-07-01
*
Ajout make_typed_lazy
herbelin
2000-06-29
*
Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constr
herbelin
2000-06-03
*
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
*
Centralisation prod_name and co dans Environ; mkLambda_string dans Term
herbelin
2000-05-18
*
Retrait de PrintConstr vers top_printers
delahaye
2000-05-03
*
diverses modifs pour ocamlweb
filliatr
2000-05-03
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'
herbelin
2000-05-02
*
Déplacement du type reference dans Term
herbelin
2000-04-28
*
Abstraction du type typed_type (un pas vers les jugements 2 niveaux)
herbelin
2000-04-20
*
Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...
herbelin
2000-03-21
*
Ajout destApplication
herbelin
2000-03-07
*
MAJ ocaml 2.99 (espaces dans la syntaxe des cast)
herbelin
2000-01-26
[next]