diff options
| author | Pierre-Marie Pédrot | 2017-08-02 01:59:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 02:00:42 +0200 |
| commit | c96b746b17a37e242fc01103d22fa0b852da84c5 (patch) | |
| tree | 26d9151e9413a68913aec575ba33f5297afe8908 /src | |
| parent | 087012f8d3e5e31f489e35dce8397b5202c928b6 (diff) | |
Bindings use open constr quotations.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 13d5dba8c6..3c41828cd3 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -301,18 +301,18 @@ GEXTEND Gram ; simple_binding: [ [ "("; LEFTQMARK; id = Prim.ident; ":="; c = Constr.lconstr; ")" -> - Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), Tac2quote.of_constr ~loc:!@loc c) + Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), Tac2quote.of_open_constr ~loc:!@loc c) | "("; n = Prim.natural; ":="; c = Constr.lconstr; ")" -> - Loc.tag ~loc:!@loc (QExpr (AnonHyp n), Tac2quote.of_constr ~loc:!@loc c) + Loc.tag ~loc:!@loc (QExpr (AnonHyp n), Tac2quote.of_open_constr ~loc:!@loc c) | "("; id = Prim.ident; ":="; c = Constr.lconstr; ")" -> - Loc.tag ~loc:!@loc (QExpr (NamedHyp id), Tac2quote.of_constr ~loc:!@loc c) + Loc.tag ~loc:!@loc (QExpr (NamedHyp id), Tac2quote.of_open_constr ~loc:!@loc c) ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> QExplicitBindings bl | bl = LIST1 Constr.constr -> - let bl = List.map (fun c -> Tac2quote.of_constr ~loc:!@loc c) bl in + let bl = List.map (fun c -> Tac2quote.of_open_constr ~loc:!@loc c) bl in QImplicitBindings bl ] ] ; |