aboutsummaryrefslogtreecommitdiff
path: root/test-suite/complexity/injection.v
AgeCommit message (Expand)Author
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2013-01-21Last test-suite not in Symmetric Patterns syntaxpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-04illegal tactic application was having Ltac interpreter loopbarras
2007-04-14Ajout d'un test de complexité de injection (cf bug 1173)herbelin