aboutsummaryrefslogtreecommitdiff
path: root/tactics/contradiction.mli
AgeCommit message (Expand)Author
2015-01-12Update headers.Maxime Dénès
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2012-08-08Updating headers.herbelin
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-12-21Generic support for open terms in tacticsherbelin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2004-07-16Nouvelle en-têteherbelin
2003-10-19Extension de l'utilisation de contradictionherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 12:36:52 +0000