aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* discriminate: Do fresh_global in the right env in presence of side-effects.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedGravatar Hugo Herbelin2015-09-08
* Fixing bug #4216:Gravatar Pierre-Marie Pédrot2015-05-13
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forGravatar Hugo Herbelin2015-05-09
* Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Gravatar Hugo Herbelin2015-05-06
* Fixing "subst" to respect v8.4 most-ancient to most-recent hyps orderGravatar Hugo Herbelin2015-05-06
* Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18
* Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toGravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* In Hipattern: some functions not working modulo evar instantiation.Gravatar Arnaud Spiwack2014-08-07
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* Remove spurious [1] in equality.ml.Gravatar Arnaud Spiwack2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Fix program cases and inversion tactic to correctly record universe constraints.Gravatar Matthieu Sozeau2014-06-24
* Removing opens to Clenvtac to track its use more easily.Gravatar Pierre-Marie Pédrot2014-06-23
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
* When discrimination is not possible, try to project.Gravatar Maxime Dénès2014-05-18
* Suggest Set Injection On Proofs in error message for injection.Gravatar Maxime Dénès2014-05-18
* Restored old behavior of injection on proofs by default.Gravatar Maxime Dénès2014-05-18
* Code cleaning & factorizing functions in Equality.Gravatar Pierre-Marie Pédrot2014-05-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:31:41 +0000