aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml4
AgeCommit message (Expand)Author
2013-09-26Splitting Rewrite into a code part and a CAMLP4-dependent one.ppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-07-17Pre-create typeclass_instances and rewrite hintdb in Autoletouzey
2013-06-22Now, idtac closures use maps instead of association list.ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-19- Keep the refinement of existing evars comming from unification with a rewri...msozeau
2013-06-14Using an "extra" Store.t field in interp_sign instead of dedicatedppedrot
2013-06-14When doing setoid_rewrite through rewrite, do resolution of classesmsozeau
2013-06-12Fixing a Not_found and evar not found anomaly found in ATBR,msozeau
2013-06-12One more fix for rewrite: disallow resolving of the (partial) constraintsmsozeau
2013-06-10Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...msozeau
2013-06-07Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd msozeau
2013-06-06Uniformizing generic argument types.ppedrot
2013-06-04Start documenting new [rewrite_strat] tactic that applies rewritingmsozeau
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