diff options
author | 2006-01-11 09:04:44 +0000 | |
---|---|---|
committer | 2006-01-11 09:04:44 +0000 | |
commit | 88d15de0cc467368dc71851e995d82093f9692ca (patch) | |
tree | 3f3410745edcb74f9c6a1c41be3691b71e544873 | |
parent | 3768be5b5416c5c4ea159e5d8779f8393ada733a (diff) |
Ajout paramétricité du nom de la base de hint dans auto et trivial
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7836 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -32,6 +32,7 @@ Ltac goal with"). - New modifier "lazy" (TODO) for "match t with" and "match goal with" telling to delay the evaluation of tactic expression. +- Hint base name can be parametric in auto and trivial. Tactics |