aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* Removing the last Evd.diff from Hints.Gravatar Pierre-Marie Pédrot2014-10-27
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Ensuring compatibility when an hypothesis used for destruct isGravatar Hugo Herbelin2014-10-27
* Fixing evars lost in interpretation of eliminator of destruct.Gravatar Hugo Herbelin2014-10-27
* Preventing potential evar leak in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-26
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* Dead code + typo.Gravatar Hugo Herbelin2014-10-26
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Apparently, the former refine was simplifying in hypotheses too.Gravatar Hugo Herbelin2014-10-24
* Addressing report #3279 (inconsistency of behavior of the -> and <-Gravatar Hugo Herbelin2014-10-24
* Specializing tclBREAK so that it can choose the return exception in caseGravatar Pierre-Marie Pédrot2014-10-22
* Refine tactic: simplify the conclusion only at the end of the tactic.Gravatar Arnaud Spiwack2014-10-22
* Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].Gravatar Arnaud Spiwack2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
* 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
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Remove duplicate code.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
* Removing re-typecheking from "refine" in no-check mode of the newGravatar Hugo Herbelin2014-10-20
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* Relaxing again the test on types of replacements in tactic changeGravatar Hugo Herbelin2014-10-16
* In convert_concl/convert_hyp: nf_enter -> enter.Gravatar Hugo Herbelin2014-10-16
* Refresh to avoid algebraic universes on the right.Gravatar Matthieu Sozeau2014-10-16
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* Fix for bug #3618.Gravatar Matthieu Sozeau2014-10-15
* Remaining tactics of the Auto module were put in the monad.Gravatar Pierre-Marie Pédrot2014-10-15
* Fix bug #3698: stack overflow due to eta+canonical structures inGravatar Matthieu Sozeau2014-10-14
* Fixing "change" and "fold" after convert_hyp/convert_concl moved toGravatar Hugo Herbelin2014-10-13
* Add support for deactivating type class inference from induction/destruct.Gravatar Hugo Herbelin2014-10-13
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* Propagating name of goal to main subgoal in cut and conversion tactics.Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Removing debugging information committed by mistake.Gravatar Hugo Herbelin2014-10-07
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
* Semantic fix of a refine in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-05
* Check compatibility of types in change depending on whether it is aGravatar Hugo Herbelin2014-10-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 10:42:18 +0000