aboutsummaryrefslogtreecommitdiff
path: root/tactics/contradiction.ml
AgeCommit message (Expand)Author
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-29Removing the evar_map argument from s_enter.Pierre-Marie Pédrot
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-20Renaming Goal.enter field into s_enter.Pierre-Marie Pédrot
2015-10-19Removing tclEVARS in various places.Pierre-Marie Pédrot
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-04-23Using tclZEROMSG instead of tclZERO in several places.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-01Removing some tactic compatibility layer.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-03-19Using non-normalized goals in tactic interpretation.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-28Evar leak in "absurd" tactic.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-14Second step of integration of Program:msozeau
2012-03-02Noise for nothingpboutill
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 23:01:29 +0000