index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Simplification du filtrage si la premiere ligne de motifs est inevitable + au...
herbelin
2002-05-03
*
Minor correction of get_lem_name
coq
2002-05-02
*
nettoyage code
courant
2002-05-02
*
petit bug dans les noms de fichiers
letouzey
2002-04-24
*
lemmes sur Zdiv/Zmod
filliatr
2002-04-19
*
jLogic disparaît
herbelin
2002-04-19
*
un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...
filliatr
2002-04-19
*
Suppression d'un warning plus surprenant qu'utile
herbelin
2002-04-18
*
*** empty log message ***
letouzey
2002-04-18
*
*** empty log message ***
werner
2002-04-17
*
Ajout remarques diverses et tactiques
herbelin
2002-04-17
*
typed unification in the case of Pattern
barras
2002-04-17
*
Quelques bugs avec inject_nat
herbelin
2002-04-17
*
jLogic.mli remplace par jolic.mli
herbelin
2002-04-17
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
*** empty log message ***
courant
2002-04-17
*
Déplacement/renommage de Class.stre_max en Declare.strength_min
herbelin
2002-04-16
*
Typo
herbelin
2002-04-16
*
Refine the procedure that generalizes context to current goal.
huang
2002-04-15
*
integration de coq-inferior par Marco Maggesi
filliatr
2002-04-15
*
coq-inferior, by Marco Maggesi
filliatr
2002-04-15
*
maj doc extraction dans repertoire contrib/extraction
letouzey
2002-04-15
*
backtrack unification
barras
2002-04-12
*
Intuition
courant
2002-04-12
*
q: Commande introuvable.
herbelin
2002-04-12
*
*** empty log message ***
courant
2002-04-12
*
*** empty log message ***
herbelin
2002-04-12
*
Interdiction de nommer une constante comme une variable de section (plus simp...
herbelin
2002-04-12
*
maj test des reals
letouzey
2002-04-12
*
petit bug avec dummy_lams
letouzey
2002-04-12
*
Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannion
herbelin
2002-04-12
*
Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...
herbelin
2002-04-11
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
Simplification du nom de l'architecture Mac OS X
herbelin
2002-04-10
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
backtrack dans l'algo d'unification
barras
2002-04-10
*
Syntactic Definition autorisée dans les motifs de Cases (utile notamment
herbelin
2002-04-10
*
MAJ
herbelin
2002-04-10
*
Simplification des Clear internes dégénérés (sans hypothèses à effacer)
herbelin
2002-04-10
*
MAJ
herbelin
2002-04-10
*
package camlindent inutilise
barras
2002-04-10
*
extraction.ml
letouzey
2002-04-08
*
babioles de renommages
letouzey
2002-04-08
*
Zdiv -> Export ZArith
filliatr
2002-04-08
*
syntaxe pour Zdiv et Zmod
filliatr
2002-04-08
*
ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...
letouzey
2002-04-08
*
*** empty log message ***
courant
2002-04-08
*
export de la fonction Reductionops.find_conclusion pour l'extraction
letouzey
2002-04-08
*
Suppression de l'application de f_equal2 pour "mult" (non inversible);
herbelin
2002-04-05
[next]