diff options
| author | Pierre-Marie Pédrot | 2017-08-29 18:32:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-29 19:37:11 +0200 |
| commit | 63d36d429edd2e85cbebe69f66e8949b25b46c70 (patch) | |
| tree | 3e061c4920249705be01d66f9fcdfe2ba67bb26b /src/tac2expr.mli | |
| parent | 31e686c2904c3015eaec18ce502d4e8afe565850 (diff) | |
Rolling our own generic arguments.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 0b02ba2656..ccff8e7756 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -104,7 +104,7 @@ type raw_tacexpr = | CTacRec of Loc.t * raw_recexpr | CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid | CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr -| CTacExt of Loc.t * raw_generic_argument +| CTacExt : Loc.t * ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr and raw_taccase = raw_patexpr * raw_tacexpr @@ -132,7 +132,7 @@ type glb_tacexpr = | GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr | GTacOpn of ltac_constructor * glb_tacexpr list | GTacWth of glb_tacexpr open_match -| GTacExt of glob_generic_argument +| GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr | GTacPrm of ml_tactic_name * glb_tacexpr list (** {5 Parsing & Printing} *) |