aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/contradiction.ml
Commit message (Expand)AuthorAge
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Using non-normalized goals in tactic interpretation.Gravatar Pierre-Marie Pédrot2014-03-19
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Porting Tactics.assumption to the new engine.Gravatar ppedrot2013-11-08
* Made Proofview.Goal.hyps a named_context.Gravatar aspiwack2013-11-02
* Less use of the list-based interface for goal-bound tactics.Gravatar aspiwack2013-11-02
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
* More Proofview.Goal.enter.Gravatar aspiwack2013-11-02
* Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).Gravatar aspiwack2013-11-02
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Evar leak in "absurd" tactic.Gravatar ppedrot2013-10-28
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Insère une coercion vers Sortclass dans 'contradiction' si nécessaireGravatar herbelin2006-10-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* Extension de l'utilisation de contradictionGravatar herbelin2003-10-19
* Extension de Contradiction au cas d'hypotheses ~A et A dans le contexteGravatar herbelin2003-10-18
* Pour les tactiques dépendant de FalseGravatar herbelin2002-05-29