aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Writing the raw introduction tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-11-05
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
* Subtle swap of lines to preserve VarInstance src field before checkingGravatar Hugo Herbelin2014-11-03
* Fix to 844431761 on improving elimination with indices, getting rid ofGravatar Hugo Herbelin2014-11-03
* Saving some nf_evars in the code of destruct/induction.Gravatar Hugo Herbelin2014-11-02
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Some reorganization of the code for destruct/induction:Gravatar Hugo Herbelin2014-11-02
* Plural and singular forms in error messages.Gravatar Hugo Herbelin2014-11-02
* Fixing 1177da327 (reorganization of the test for generic selection ofGravatar Hugo Herbelin2014-11-02
* Info: the warning message of the defunct [info] tactic now points to the [Inf...Gravatar Arnaud Spiwack2014-11-01
* Info: print name of calls to Ltac constants ([TacCall]).Gravatar Arnaud Spiwack2014-11-01
* Info: tactic notations (TacAlias) print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: Tactics coming from [TACTIC EXTEND] print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: print the name of atomic tactics.Gravatar Arnaud Spiwack2014-11-01
* Info: Ltac's idtac logs its message in the info trace.Gravatar Arnaud Spiwack2014-11-01
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Avoid "destruct H" to apply on H itself when H is a section variable.Gravatar Hugo Herbelin2014-10-31
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 11:26:43 +0000