aboutsummaryrefslogtreecommitdiff
path: root/tactics/hipattern.mli
AgeCommit message (Expand)Author
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-08-07In Hipattern: some functions not working modulo evar instantiation.Arnaud Spiwack
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-26Removing Tacmach compatibility layer in Inv.Pierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-04-29Merging Context and Sign.ppedrot
2012-12-18Modulification of nameppedrot
2012-08-08Updating headers.herbelin
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-03-02Noise for nothingpboutill
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-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-04Fixed subst failing when a truly heterogeneous JMeq hyp is in theherbelin
2009-08-03Added "etransitivity".herbelin
2009-05-17- Allowing multiple calls to tactic fix with automatic generation ofherbelin
2008-12-30- Fixed bugs and compatibilities issues in herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-26- Optimized "auto decomp" which had a (presumably) exponential inherbelin
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-03-22- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deherbelin
2005-03-18appel de Simplify depuis Coqcoq
2004-07-16Nouvelle en-têteherbelin
2003-06-20Ground Update.corbinea
2003-05-25Ground and CCsolve updatescorbinea
2003-05-19Restructuration des procédures de filtrageherbelin
2003-04-25Added the Ground tactic.corbinea
2002-05-22Correction of a bug in Intuition (no more decomposition of dependent pairs).corbinea
2001-09-13eclaircissement du codecourant
2001-03-15entetesfilliatr
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-05-03diverses modifs pour ocamlwebfilliatr
2000-05-03Ajout get_referenceherbelin
2000-04-30Suite intégration de constr_patternherbelin
2000-04-28Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 21:23:37 +0000