diff options
| author | herbelin | 2004-02-12 22:46:22 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-12 22:46:22 +0000 |
| commit | 5a93c2eede9d55cac569c46784543abd3732cb10 (patch) | |
| tree | a8447b8da42bf014f73495ef6e25182ecd7473d8 | |
| parent | 099ac51a6c03a5ac7178b4ea616763dac73a484e (diff) | |
Typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5331 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 809e5a2300..8a1bbd3cb0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1742,10 +1742,10 @@ and interp_atomic ist gl = function | ConstrMayEvalArgType -> VConstr (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x)) - | StringArgType | BoolArgType - | QuantHypArgType | RedExprArgType | TacticArgType -> val_interp ist gl (out_gen globwit_tactic x) + | StringArgType | BoolArgType + | QuantHypArgType | RedExprArgType | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ -> error "This generic type is not supported in alias" |