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.ml | |
| parent | 0232b0de849998d3394a4e6a2ab6232a75897610 (diff) | |
Introducing a quotation for global references.
Diffstat (limited to 'src/tac2env.ml')
| -rw-r--r-- | src/tac2env.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/tac2env.ml b/src/tac2env.ml index ac2bd5fc23..65276ec57f 100644 --- a/src/tac2env.ml +++ b/src/tac2env.ml @@ -246,7 +246,7 @@ let shortest_qualid_of_projection kn = type 'a ml_object = { ml_type : type_constant; - ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic; + ml_interp : environment -> 'a -> valexpr Proofview.tactic; } module MLTypeObj = @@ -271,8 +271,9 @@ let std_prefix = (** Generic arguments *) -let wit_ltac2 = Genarg.make0 "ltac2" +let wit_ltac2 = Genarg.make0 "ltac2:value" let wit_pattern = Genarg.make0 "ltac2:pattern" +let wit_reference = Genarg.make0 "ltac2:reference" let is_constructor qid = let (_, id) = repr_qualid qid in |