aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/ImplicitArguments.v
AgeCommit message (Expand)Author
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2018-10-04test-suite: cleaningVincent Laporte
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2017-05-31Fixing a failure to interpret some local implicit arguments in Inductive.Hugo Herbelin
2017-04-09Fixing several wrong computations of implicit arguments by positionHugo Herbelin
2013-05-08Declaration of multiple hypotheses or parameters now share typingherbelin
2013-01-18Unset Asymmetric Patternspboutill
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-03-15Forgot the test file.msozeau