aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-11-27Reverting the following block of three commits:Hugo Herbelin
2014-11-26Experimenting always forcing convertibility on strict implicit argumentsHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-13Fixing injection bug #3616 on sigma-types.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18Improving error message when applying rewrite to an expression which is not a...Hugo Herbelin
2014-08-18Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-07In Hipattern: some functions not working modulo evar instantiation.Arnaud Spiwack
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05A new step in the new "standard" naming policy for propositional hypothesesHugo Herbelin
2014-08-01Remove spurious [1] in equality.ml.Arnaud Spiwack
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-24Fix program cases and inversion tactic to correctly record universe constraints.Matthieu Sozeau
2014-06-23Removing opens to Clenvtac to track its use more easily.Pierre-Marie Pédrot
2014-05-31More on injection over a projectable "existT". - Fixing syntax "injection ......Hugo Herbelin
2014-05-31Fixing introduction patterns * and ** when used in a branch so that they do n...Hugo Herbelin
2014-05-31Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Hugo Herbelin
2014-05-18When discrimination is not possible, try to project.Maxime Dénès
2014-05-18Suggest Set Injection On Proofs in error message for injection.Maxime Dénès
2014-05-18Restored old behavior of injection on proofs by default.Maxime Dénès
2014-05-09Code cleaning & factorizing functions in Equality.Pierre-Marie Pédrot
2014-05-08Encapsulating some clausenv uses. This simplifies the control flow of somePierre-Marie Pédrot
2014-05-08Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Hugo Herbelin
2014-05-08Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Hugo Herbelin
2014-05-08Simplification and improvement of "subst x" in such a way that itHugo Herbelin
2014-05-06Fixes after rebase. The use of pf_constr_of_global is problematic in presence...Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-30Trying to improve the error messages of injection.Maxime Dénès
2014-04-29Injection: do not fail when arguments have sort Prop.Maxime Dénès
2014-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-14Closing bug #3260Julien Forest
2014-03-27Cosmetic changes in Equality.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Equality.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 21:14:13 +0000