aboutsummaryrefslogtreecommitdiff
path: root/tactics/elim.mli
AgeCommit message (Expand)Author
2021-01-20Remove double induction tacticJim Fehrle
2020-09-04Statically enforce that elim is passed a fully applied inductive type.Pierre-Marie Pédrot
2020-09-04Enforce the argument of elim functions to be a variable.Pierre-Marie Pédrot
2020-09-02Factorize the only uses of internal API in Elim for Inv.Pierre-Marie Pédrot
2020-09-02Make the Elim.branch_args type opaque.Pierre-Marie Pédrot
2020-09-02Further remove the type Elim.branch_assumptions.Pierre-Marie Pédrot
2020-09-02Remove unused API from Elim.Pierre-Marie Pédrot
2020-08-31Move elim-specific code from Tacticals to Elim.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-06-12[api] Misctypes removal: tactic flags.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-02-14Elim API using EConstr.Pierre-Marie Pédrot
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
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-12-14Modulification of identifierppedrot
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-02Noise for nothingpboutill
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-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-08-04Évolutions diverses et variées.herbelin
2004-07-16Nouvelle en-têteherbelin
2004-03-01Déplacement définition intro_pattern_expr dans Genargherbelin
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-08-05Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-05-03Ajout du langage de tactiquesdelahaye
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:47 +0000