aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.ml4
Commit message (Expand)AuthorAge
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Some cleanup in AutoGravatar ppedrot2013-09-03
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* More functional implementation of locality_flag and program_modeGravatar gareuselesinge2013-04-15
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* More cleaningGravatar ppedrot2012-06-01
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
* Remove print call that do not use the pp mechanismGravatar pboutill2012-04-12
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* Noise for nothingGravatar pboutill2012-03-02
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* auto with nocore : disable the use of the core database (wish #2188)Gravatar letouzey2011-09-23
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
* - Allow to set a particular transparent_state for the local hintGravatar msozeau2011-03-04
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Minor fixes:Gravatar msozeau2010-07-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Avoid computing tactic printing tree (std_ppcmds) when printing not needed inGravatar herbelin2010-06-03
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Use nice "unfold" instead of ugly "change" to display calls to unfold hintsGravatar herbelin2010-04-17
* Fix [autounfold] to accept general [in] clauses.Gravatar msozeau2010-03-05
* Misc fixes.Gravatar msozeau2009-11-06
* 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
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27