aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
Commit message (Expand)AuthorAge
...
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Fix bug #1977 by allowing the [apply] variants to take an [open_constr]Gravatar msozeau2008-10-23
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* Improve typeclasses eauto using the dnet for local assumptions too, and selectGravatar msozeau2008-09-04
* Little cleanup in auto.Gravatar msozeau2008-08-27
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Suite commit 11236Gravatar notin2008-07-24
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Fix implicit arguments in sections bug and check for resolution of evars whenGravatar msozeau2008-07-07
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandGravatar herbelin2008-04-04
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Mise en place d'une toute petite amélioration de l'unification deGravatar herbelin2008-02-07
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26