aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml4
Commit message (Expand)AuthorAge
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More cleaning in CArray...Gravatar ppedrot2012-09-18
* 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
* Fix typeclass error handling which was sometimes raising a Failure ("hd").Gravatar msozeau2012-07-11
* Better treatment of error messages in rewrite (avoid use of Errors.print).Gravatar msozeau2012-07-10
* rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteGravatar letouzey2012-07-05
* Fixes in rewriting by strategies (almost ready to be documented!):Gravatar msozeau2012-07-05
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri...Gravatar msozeau2012-06-19
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar 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
* Corrects a (very) longstanding bug of tactics. As is were, tactic expectingGravatar aspiwack2012-04-18
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Noise for nothingGravatar pboutill2012-03-02
* In [reflexivity], [symmetry] etc, use the type found by looking at the relati...Gravatar msozeau2012-02-14
* Fix bug #2483: anomaly raised due to wrong handling of the evars state.Gravatar msozeau2012-01-23
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
* Proof using ...Gravatar gareuselesinge2011-12-12
* Merge fix for bug #2604.Gravatar msozeau2011-11-17
* Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...Gravatar msozeau2011-11-17
* Was missing a potential application of subtypingGravatar msozeau2011-11-17
* Fix bug #2473 due to wrong folding of the evar environmentGravatar msozeau2011-10-18
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Remove duplicated version of check_required_library.Gravatar letouzey2011-09-22
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...Gravatar msozeau2011-06-07
* Add a flag to control betaiota reduction during unification to maintain backw...Gravatar msozeau2011-04-18
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
* Fix declarations of [Add Setoid/Morphism...] in sections to not exportGravatar msozeau2011-03-08
* - Allow rewriting under abitrary products, not just those in Prop.Gravatar msozeau2011-02-28
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* Change Evd.fold to a faster version that simply removes unneeded evars.Gravatar msozeau2011-02-11
* - proper printing of setoid_rewrite tactic applicationsGravatar msozeau2011-02-10
* Rename subst_raw_with_bindings to subst_glob_with_bindings and exportGravatar msozeau2011-02-10