aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenvtac.ml
Commit message (Expand)AuthorAge
* - Fixed a bug in checking that implicit arguments are all correctlyGravatar herbelin2009-09-18
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* Minor unification changes:Gravatar msozeau2009-05-18
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* More debugging of handling of open constrs with typeclasses:Gravatar msozeau2008-10-25
* Raise informative errors instead of Failures or anomalies in case a metaGravatar msozeau2008-10-24
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* Changement des named_contextGravatar gregoire2005-12-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* simplification de clenvGravatar barras2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03