diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-22 00:58:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-22 01:03:44 +0200 |
| commit | 9c927ebdd7e72bb4ae39b549f55f375d66683be5 (patch) | |
| tree | 3952c62a17e4b73986d5f2bb52034cd8ae57fa6e /interp | |
| parent | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (diff) | |
Removing useless use of metaids in tactic AST.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrarg.mli b/interp/constrarg.mli index d5d19f2ea..983163ec1 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -70,4 +70,4 @@ val wit_red_expr : val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type -val wit_clause_dft_concl : (Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type +val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type |