aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-09Redo fix init_setoid -> init_relation_classesMatthieu Sozeau
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-28Fixing bug #4596: [rewrite] broke in the past few weeks.Pierre-Marie Pédrot
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-19Fix regression from 8.4 in reflexivity/...Matthieu Sozeau
2016-02-17Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Matthieu Sozeau
2016-01-07Fix bug #4480: progress was not checked for setoid_rewrite.Matthieu Sozeau
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-04Fix in setoid_rewrite in Type: avoid the generation of a rigid universeMatthieu Sozeau
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-13Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Matthieu Sozeau
2015-11-11Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Matthieu Sozeau
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Remove code that was already commented out.Maxime Dénès
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-09-22Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.Pierre-Marie Pédrot
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-06-23With the field record punning syntax.Theo Zimmermann
2015-06-23Put all arguments of strategy in record.Theo Zimmermann
2015-06-23Strategy is now a record type with a function field.Theo Zimmermann
2015-06-23Add comments.Theo Zimmermann
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-11Fixing bug #4232.Pierre-Marie Pédrot
2015-05-05Removing dead code in Rewrite.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-02-18Fix bug #3938Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 13:12:33 +0000