aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml
AgeCommit message (Expand)Author
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
2016-04-07Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-02-28Fixing bug #4596: [rewrite] broke in the past few weeks.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-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
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-04Fix in setoid_rewrite in Type: avoid the generation of a rigid universeMatthieu Sozeau
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-28Univs: local names handling.Matthieu Sozeau
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
2015-02-16Fixing bug #3944.Pierre-Marie Pédrot
2015-02-14Fixing bug #4016.Pierre-Marie Pédrot
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2015-01-06Fix setoid rewrite.Arnaud Spiwack
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-02For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaPierre-Marie Pédrot
2014-12-01More invariants in the code of Rewrite.Pierre-Marie Pédrot
2014-11-30Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Hugo Herbelin
2014-11-22Attempt to organize and document unification flags of setoid rewrite.Hugo Herbelin
2014-11-22In setoid_rewrite error messages:Hugo Herbelin
2014-11-22Fix resolve_morphism to build well-scoped terms in case some argumentsMatthieu Sozeau
2014-11-18Tentative rephrasing of error message for rewrite.Hugo Herbelin
2014-11-10Replugging hints in rewriting strategies.Pierre-Marie Pédrot
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-10-27Cleaning and documenting Clenv.make_evar_clausePierre-Marie Pédrot
2014-10-26Preventing potential evar leak in Rewrite.Pierre-Marie Pédrot
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-21Removing dead code in Rewrite.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:27:13 +0000