diff options
| author | ppedrot | 2013-07-02 14:46:47 +0000 |
|---|---|---|
| committer | ppedrot | 2013-07-02 14:46:47 +0000 |
| commit | 89abe2a141b3baa11bf0e8bcdecaf68220251c6e (patch) | |
| tree | 70e457c39239837c84435d3146af35d1190a4225 /grammar | |
| parent | 20f84d1e80a934c50bae81b1a017f12f26997ded (diff) | |
Removed the ad-hod handling of wit_tacticn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16615 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index eb4630394b..dfcaa4e84c 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -22,14 +22,11 @@ let qualified_name loc s = qualified_name loc path name let mk_extraarg loc s = - if Extrawit.tactic_genarg_level s = None then - try - let name = Genarg.get_name0 s in - qualified_name loc name - with Not_found -> - <:expr< $lid:"wit_"^s$ >> - else - qualified_name loc ("Extrawit.wit_" ^ s) + try + let name = Genarg.get_name0 s in + qualified_name loc name + with Not_found -> + <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >> |