aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Notations:Gravatar herbelin2006-10-09
* Remplacement des nf_evar (source de complexité polynomiale) par de laGravatar herbelin2006-10-06
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
* Suppression d'une source de complexité polynomiale dans le pretypageGravatar herbelin2006-10-06
* Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...Gravatar notin2006-10-05
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* Ajout allowed_sortsGravatar herbelin2006-10-01
* Correction d'un bug de coercion de pattern introduit dans la 8.1betaGravatar herbelin2006-09-23
* Correction bug #1168 (dans les coercions de pattern, c'est le nombreGravatar herbelin2006-09-23
* Wish #1187 granted (support for canonical structures that are recordsGravatar herbelin2006-09-23
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Débogage: ajout affichage contraintes d'unificationGravatar herbelin2006-09-15
* Abandon unification pattern des evars dans apply: combiné avec leGravatar herbelin2006-09-13
* Correction conflit Meta/Evar dans commit précédent et extension auGravatar herbelin2006-09-12
* Ajout unification pattern dans l'algorithme d'unification desGravatar herbelin2006-09-12
* Workaround Map.fold semantic change in ocaml-3.08.4 and higher.Gravatar msozeau2006-09-05
* Ajout is_sort: test si se réduit en une sorteGravatar herbelin2006-09-01
* Export de check_evars vers command.mlGravatar herbelin2006-09-01
* Ajout (pour complétude) du cas d'inversion d'un pattern de Miller visGravatar herbelin2006-08-29
* Prise en compte de l'instance des evars dans la détection des 'motifs'Gravatar herbelin2006-08-29
* Il faut (au moins) normaliser les evars avant de tenterGravatar herbelin2006-08-29
* Diverses modifications autour de l'unification modulo conversion:Gravatar herbelin2006-08-28
* Ajout whd_eta + export append_stack_list + petit nettoyage (dont maj de Gravatar herbelin2006-08-28
* Morceau de code mortGravatar herbelin2006-08-24
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Correction bug 1172 + correction en passant de la taille des paramètres de f...Gravatar herbelin2006-07-07
* Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...Gravatar herbelin2006-06-27
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
* bug serieux efficacite de ltacGravatar barras2006-06-19
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
* Correcting a bug in matching context on if. Gravatar jforest2006-05-17
* Code mortGravatar herbelin2006-05-13
* correction bugs dans Cbv (beta n-aire)Gravatar barras2006-05-10
* subst. explicites avec vecteursGravatar barras2006-05-09
* amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)Gravatar barras2006-05-05
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Typo dans précédent commit (8755); protection renforcée dans analyse claus...Gravatar herbelin2006-04-28
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* - Utilisation d'abbréviations pour les types intervenant dans RCasesGravatar herbelin2006-04-26
* Reverting nf_betaiotaevar_preserving_vm_castGravatar jforest2006-04-25
* Code mort (suite)Gravatar herbelin2006-04-25
* Suppression code mortGravatar herbelin2006-04-25
* Timide tentative de clarification du statut de l'opérateur de filtrageGravatar herbelin2006-04-24
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14