diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-26 15:50:37 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-26 15:50:37 +0000 |
| commit | 2d08ea6e2563bb10170f904f6e527bdec02f2432 (patch) | |
| tree | 50c32e27c519def3c67a51473cdee732d4961815 /tactics | |
| parent | 6bf3d8dbccdfa4b072eb6bef1d0480a678f0817e (diff) | |
backtrack of the last commit (it was my fault: the code is used by
camlp4-generated code even if it is not found using grep)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6351 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 0e6760b31..8d8d12fb4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -94,6 +94,9 @@ val intern_constr : val intern_hyp : glob_sign -> identifier Util.located -> identifier Util.located +val subst_genarg : + substitution -> glob_generic_argument -> glob_generic_argument + val subst_rawconstr : substitution -> rawconstr_and_expr -> rawconstr_and_expr |