aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.mli
Commit message (Expand)AuthorAge
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Updating headers.Gravatar herbelin2012-08-08
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
* Fix [autounfold] to accept general [in] clauses.Gravatar msozeau2010-03-05
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)Gravatar jforest2008-03-08
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* Work-in-progress to make eauto accept a list of goals as input andGravatar msozeau2008-02-06
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
* Export de simplest_eapply, utilisé dans la contrib interfaceGravatar notin2007-04-16
* Suite unification apply et eapply (l'un et l'autre profite maintenantGravatar herbelin2007-04-16
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* A la demande de Julien ForestGravatar letouzey2005-11-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* Interface EautoGravatar herbelin2003-09-18