aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml
Commit message (Expand)AuthorAge
* Fix in setoid_rewrite in Type: avoid the generation of a rigid universeGravatar Matthieu Sozeau2015-12-04
* Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Gravatar Matthieu Sozeau2015-11-13
* Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Gravatar Matthieu Sozeau2015-11-11
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Remove code that was already commented out.Gravatar Maxime Dénès2015-10-12
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.Gravatar Pierre-Marie Pédrot2015-09-22
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* With the field record punning syntax.Gravatar Theo Zimmermann2015-06-23
* Put all arguments of strategy in record.Gravatar Theo Zimmermann2015-06-23
* Strategy is now a record type with a function field.Gravatar Theo Zimmermann2015-06-23
* Add comments.Gravatar Theo Zimmermann2015-06-23
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Fixing bug #4232.Gravatar Pierre-Marie Pédrot2015-05-11
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2015-05-05
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Fix bug #3938Gravatar Matthieu Sozeau2015-02-18
* Fixing bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
* Fixing bug #4016.Gravatar Pierre-Marie Pédrot2015-02-14
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix setoid rewrite.Gravatar Arnaud Spiwack2015-01-06
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaGravatar Pierre-Marie Pédrot2014-12-02
* More invariants in the code of Rewrite.Gravatar Pierre-Marie Pédrot2014-12-01
* Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Gravatar Hugo Herbelin2014-11-30
* Attempt to organize and document unification flags of setoid rewrite.Gravatar Hugo Herbelin2014-11-22
* In setoid_rewrite error messages:Gravatar Hugo Herbelin2014-11-22
* Fix resolve_morphism to build well-scoped terms in case some argumentsGravatar Matthieu Sozeau2014-11-22
* Tentative rephrasing of error message for rewrite.Gravatar Hugo Herbelin2014-11-18
* Replugging hints in rewriting strategies.Gravatar Pierre-Marie Pédrot2014-11-10
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* Preventing potential evar leak in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-26
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Small invariants in Rewrite code.Gravatar Pierre-Marie Pédrot2014-10-21
* Fixing decompose_app_rel in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Using new clausenv in rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Semantic fix of a refine in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-05
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteGravatar Matthieu Sozeau2014-09-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 23:26:45 +0000