aboutsummaryrefslogtreecommitdiff
path: root/tactics/hipattern.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-06unsafe_type_of -> type_of in Tactics.intro_decomp_eq (hipattern changes)Gaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2017-12-07Getting rid of pf_matches in Hipattern.Pierre-Marie Pédrot
2017-07-31Remove references to Global.env in tactics/*.mlamblaf
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-29tactics cleanup: remove constr_of_global callsMatthieu Sozeau
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Do not ask for a normalized goal to get hypotheses and conclusions.Pierre-Marie Pédrot
2017-02-14Eqdecide API using EConstr.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:23 +0000