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
...
*
Correction de deux cas où les types inductifs n'étaient pas comparés
herbelin
2006-10-05
*
Ajout allowed_sorts
herbelin
2006-10-01
*
Correction d'un bug de coercion de pattern introduit dans la 8.1beta
herbelin
2006-09-23
*
Correction bug #1168 (dans les coercions de pattern, c'est le nombre
herbelin
2006-09-23
*
Wish #1187 granted (support for canonical structures that are records
herbelin
2006-09-23
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Report de l'heuristique d'unification premier ordre flexible/rigide
herbelin
2006-09-15
*
Débogage: ajout affichage contraintes d'unification
herbelin
2006-09-15
*
Abandon unification pattern des evars dans apply: combiné avec le
herbelin
2006-09-13
*
Correction conflit Meta/Evar dans commit précédent et extension au
herbelin
2006-09-12
*
Ajout unification pattern dans l'algorithme d'unification des
herbelin
2006-09-12
*
Workaround Map.fold semantic change in ocaml-3.08.4 and higher.
msozeau
2006-09-05
*
Ajout is_sort: test si se réduit en une sorte
herbelin
2006-09-01
*
Export de check_evars vers command.ml
herbelin
2006-09-01
*
Ajout (pour complétude) du cas d'inversion d'un pattern de Miller vis
herbelin
2006-08-29
*
Prise en compte de l'instance des evars dans la détection des 'motifs'
herbelin
2006-08-29
*
Il faut (au moins) normaliser les evars avant de tenter
herbelin
2006-08-29
*
Diverses modifications autour de l'unification modulo conversion:
herbelin
2006-08-28
*
Ajout whd_eta + export append_stack_list + petit nettoyage (dont maj de
herbelin
2006-08-28
*
Morceau de code mort
herbelin
2006-08-24
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22
*
Correction bug 1172 + correction en passant de la taille des paramètres de f...
herbelin
2006-07-07
*
Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...
herbelin
2006-06-27
*
Added {measure x f} as a valid recursion order.
msozeau
2006-06-22
*
bug serieux efficacite de ltac
barras
2006-06-19
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
herbelin
2006-05-28
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
Correcting a bug in matching context on if.
jforest
2006-05-17
*
Code mort
herbelin
2006-05-13
*
correction bugs dans Cbv (beta n-aire)
barras
2006-05-10
*
subst. explicites avec vecteurs
barras
2006-05-09
*
amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)
barras
2006-05-05
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Typo dans précédent commit (8755); protection renforcée dans analyse claus...
herbelin
2006-04-28
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
- Utilisation d'abbréviations pour les types intervenant dans RCases
herbelin
2006-04-26
*
Reverting nf_betaiotaevar_preserving_vm_cast
jforest
2006-04-25
*
Code mort (suite)
herbelin
2006-04-25
*
Suppression code mort
herbelin
2006-04-25
*
Timide tentative de clarification du statut de l'opérateur de filtrage
herbelin
2006-04-24
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
Pas fier
herbelin
2006-04-14
*
replacing whd_betaiotaevar_preserving_vm_cast
jforest
2006-04-14
*
Fixes for new unification, not used in default version as it really changes u...
msozeau
2006-04-10
*
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...
msozeau
2006-04-10
*
- Documentation of the Program tactics.
msozeau
2006-04-07
[prev]
[next]