aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml4
AgeCommit message (Expand)Author
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09Uniformization: isevars -> evdref/sigma/evdherbelin
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-15anew_instance should not consume the locality twicegareuselesinge
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-03-22Fix bug# 2994, 2971 about better error messages.msozeau
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-18More cleaning in CArray...ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-07-11Fix typeclass error handling which was sometimes raising a Failure ("hd").msozeau
2012-07-10Better treatment of error messages in rewrite (avoid use of Errors.print).msozeau
2012-07-05rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteletouzey
2012-07-05Fixes in rewriting by strategies (almost ready to be documented!):msozeau
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-19Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri...msozeau
2012-05-30Getting rid of Pp.msgppedrot
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-04-18Corrects a (very) longstanding bug of tactics. As is were, tactic expectingaspiwack
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-02Noise for nothingpboutill
2012-02-14In [reflexivity], [symmetry] etc, use the type found by looking at the relati...msozeau
2012-01-23Fix bug #2483: anomaly raised due to wrong handling of the evars state.msozeau
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-12-12Proof using ...gareuselesinge
2011-11-17Merge fix for bug #2604.msozeau
2011-11-17Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...msozeau
2011-11-17Was missing a potential application of subtypingmsozeau
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin