diff options
| author | Pierre-Marie Pédrot | 2017-08-24 14:58:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-24 15:41:15 +0200 |
| commit | 7d496e618f35a17b8432ac3c7205138f03c95fd2 (patch) | |
| tree | 747295c3a1364d96bc446abc491a53da3322729f /src/tac2env.mli | |
| parent | 0232b0de849998d3394a4e6a2ab6232a75897610 (diff) | |
Introducing a quotation for global references.
Diffstat (limited to 'src/tac2env.mli')
| -rw-r--r-- | src/tac2env.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/tac2env.mli b/src/tac2env.mli index e4cc8387c5..20bf24d19d 100644 --- a/src/tac2env.mli +++ b/src/tac2env.mli @@ -100,7 +100,7 @@ val interp_primitive : ml_tactic_name -> ml_tactic type 'a ml_object = { ml_type : type_constant; - ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic; + ml_interp : environment -> 'a -> valexpr Proofview.tactic; } val define_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object -> unit @@ -118,7 +118,12 @@ val std_prefix : ModPath.t val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type -val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern, Pattern.constr_pattern) genarg_type +val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern, Util.Empty.t) genarg_type + +val wit_reference : (reference, Globnames.global_reference, Util.Empty.t) genarg_type +(** Beware, at the raw level, [Qualid [id]] has not the same meaning as + [Ident id]. The first is an unqualified global reference, the second is + the dynamic reference to id. *) (** {5 Helper functions} *) |