diff options
Diffstat (limited to 'tactics/Inv.v')
| -rw-r--r-- | tactics/Inv.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/Inv.v b/tactics/Inv.v index 1abcdd824..62c77dc8a 100644 --- a/tactics/Inv.v +++ b/tactics/Inv.v @@ -68,14 +68,14 @@ Grammar vernac vernac: ast := | der_inv_clr_with [ "Derive" "Inversion_clear" identarg($na) "with" constrarg($com) "." ] - -> [(MakeInversionLemma $na $com (COMMAND (PROP{Null})))] + -> [(MakeInversionLemma $na $com (CONSTR (PROP))) ] | der_inv_with_srt [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "Sort" sortarg($s) "." ] -> [(MakeSemiInversionLemma $na $com $s)] | der_inv_with [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "." ] - -> [(MakeSemiInversionLemma $na $com (COMMAND (PROP{Null})))] + -> [(MakeSemiInversionLemma $na $com (CONSTR (PROP)))] | der_inv [ "Derive" "Inversion" identarg($na) identarg($id) "." ] -> [(MakeSemiInversionLemmaFromHyp 1 $na $id)] |