index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
Correction bugs commit précédent
herbelin
2005-12-22
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)
herbelin
2005-11-21
*
Correction de la correction du test sur le nombre de parametres d'une projection
herbelin
2005-11-19
*
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
*
Conséquences nettoyage pretyping.ml
herbelin
2005-09-09
*
Prise en compte de l'utilisation des notations récursives pour faire une not...
herbelin
2005-06-03
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...
herbelin
2005-05-20
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
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
*
Bug affichage rawconstr
herbelin
2005-02-07
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Pour cible make doc
herbelin
2005-01-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
HUGE COMMIT
sacerdot
2005-01-03
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-03
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-25
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...
herbelin
2004-12-22
*
Restauration type casted_open_constr pour tactique refine car l'unification n...
herbelin
2004-12-09
*
Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...
herbelin
2004-12-06
*
Message d'erreur
herbelin
2004-11-17
*
Suppression capture des variables par lieurs non liés dans Notation; simplif...
herbelin
2004-11-17
*
Suppression capture des variables par lieurs non liés dans Notation
herbelin
2004-11-17
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
Ajout de or-pattern pour le match-with v8
herbelin
2004-09-09
*
Interpretation et affichage corrects des notations LetTuple, affichage des no...
herbelin
2004-08-23
*
Correction bug #830 : les noms des implicites temporaires étaient inconnus a...
herbelin
2004-08-23
*
Apply implicit types to local binders too
herbelin
2004-08-06
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Suppression de Rawterm.loc, branchement sur Util.loc
herbelin
2004-07-16
*
Typo (bug #797)
herbelin
2004-06-27
*
Amélioration affichage coercions vers Funclass
herbelin
2004-06-02
*
pb facto des Fixpoint + erreur avec -dump-glob et Load
barras
2004-04-17
*
Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...
herbelin
2004-04-08
*
Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)
herbelin
2004-04-06
*
Heuristique pour traduire if-then-else quand le re-typage echoue
herbelin
2004-03-30
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...
herbelin
2004-03-27
*
Export compute_arguments_scope pour utilisation local a la construction des i...
herbelin
2004-03-27
*
Bug protection array_fold_left2
herbelin
2004-03-19
[next]