aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* In discrimination nets, do not index lambdas if they're part of a betaGravatar Matthieu Sozeau2014-12-12
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Fix dummy argument use in guess_elim: there are some cases where X_indGravatar Matthieu Sozeau2014-12-10
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.Gravatar Hugo Herbelin2014-12-08
* Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Gravatar Arnaud Spiwack2014-12-08
* Step 4 : atomize_thenGravatar Hugo Herbelin2014-12-07
* Step 2Gravatar Hugo Herbelin2014-12-07
* Step 1Gravatar Hugo Herbelin2014-12-07
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
* 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
* Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...Gravatar Hugo Herbelin2014-11-30
* Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Gravatar Hugo Herbelin2014-11-30
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* Used an evar name based on the local def name in "evar" tactic.Gravatar Hugo Herbelin2014-11-25
* One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Gravatar Hugo Herbelin2014-11-23
* Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc aboutGravatar Hugo Herbelin2014-11-23
* Specific printer of Evar.Set.t for ocamldebug + more information inGravatar Hugo Herbelin2014-11-22
* 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
* Further simplifying functional induction.Gravatar Hugo Herbelin2014-11-22
* Simplifying code of functional induction.Gravatar Hugo Herbelin2014-11-22
* Not using an (arbitrary) pivot anymore for re-introduction ofGravatar Hugo Herbelin2014-11-22
* New simplification of code for generalizing hypotheses in destruct.Gravatar Hugo Herbelin2014-11-22
* Removing a hack which, according to the comment, should not be necessaryGravatar Hugo Herbelin2014-11-22
* Fix resolve_morphism to build well-scoped terms in case some argumentsGravatar Matthieu Sozeau2014-11-22
* Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.Gravatar Pierre-Marie Pédrot2014-11-22
* Writing intro_replacing in the new monad.Gravatar Pierre-Marie Pédrot2014-11-22
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
* Fixing the previous commit. We had to normalize evars first.Gravatar Pierre-Marie Pédrot2014-11-20
* Somehow fixing a side-effect bug in tactics-in-terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Re-removing the Hiddentac module. For some reason it had been reintroducedGravatar Pierre-Marie Pédrot2014-11-20
* Global.env chasing in Inv.Gravatar Pierre-Marie Pédrot2014-11-20
* Adding locations to tclZEROMSG.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr]-s in [idtac] messages.Gravatar Arnaud Spiwack2014-11-19
* Tentative rephrasing of error message for rewrite.Gravatar Hugo Herbelin2014-11-18
* Hopefully the last word on having "simpl f" complying with theGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
* Renouncing to check only at the end of the call to "apply in" theGravatar Hugo Herbelin2014-11-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 14:56:07 +0000