aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.mli
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Eauto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* Moving Eauto to a simple ML file.Gravatar Pierre-Marie Pédrot2016-03-06
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* | Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Gravatar Pierre-Marie Pédrot2015-12-28
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | Partially porting eauto to the new tactic API.Gravatar Pierre-Marie Pédrot2015-02-23
|/
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* 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