diff options
| -rw-r--r-- | src/g_ltac2.ml4 | 7 | ||||
| -rw-r--r-- | src/tac2qexpr.mli | 4 | ||||
| -rw-r--r-- | src/tac2quote.ml | 6 |
3 files changed, 9 insertions, 8 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 8c7db71a47..bfef4fab8d 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -316,18 +316,17 @@ GEXTEND Gram ; simple_binding: [ [ "("; "$"; id = Prim.ident; ":="; c = Constr.lconstr; ")" -> - Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), Tac2quote.of_open_constr ~loc:!@loc c) + Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), c) | "("; n = Prim.natural; ":="; c = Constr.lconstr; ")" -> - Loc.tag ~loc:!@loc (QExpr (AnonHyp n), Tac2quote.of_open_constr ~loc:!@loc c) + Loc.tag ~loc:!@loc (QExpr (AnonHyp n), c) | "("; id = Prim.ident; ":="; c = Constr.lconstr; ")" -> - Loc.tag ~loc:!@loc (QExpr (NamedHyp id), Tac2quote.of_open_constr ~loc:!@loc c) + Loc.tag ~loc:!@loc (QExpr (NamedHyp id), c) ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> QExplicitBindings bl | bl = LIST1 Constr.constr -> - let bl = List.map (fun c -> Tac2quote.of_open_constr ~loc:!@loc c) bl in QImplicitBindings bl ] ] ; diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index 5075f2d7d4..8a61590a1d 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -19,8 +19,8 @@ type 'a or_anti = | QAnti of Id.t located type bindings = -| QImplicitBindings of raw_tacexpr list -| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * raw_tacexpr) Loc.located list +| QImplicitBindings of Constrexpr.constr_expr list +| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * Constrexpr.constr_expr) Loc.located list | QNoBindings type intro_pattern = diff --git a/src/tac2quote.ml b/src/tac2quote.ml index 9858f611fe..a053bd799f 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -98,9 +98,11 @@ let of_bindings ?loc = function | QNoBindings -> std_constructor ?loc "NoBindings" [] | QImplicitBindings tl -> + let tl = List.map (fun c -> of_open_constr ?loc c) tl in std_constructor ?loc "ImplicitBindings" [of_list ?loc tl] | QExplicitBindings tl -> - let tl = List.map (fun (loc, (qhyp, e)) -> of_pair ?loc (of_anti ?loc of_qhyp qhyp, e)) tl in + let map (loc, (qhyp, e)) = of_pair ?loc (of_anti ?loc of_qhyp qhyp, of_open_constr ?loc e) in + let tl = List.map map tl in std_constructor ?loc "ExplicitBindings" [of_list ?loc tl] let rec of_intro_pattern ?loc = function @@ -174,7 +176,7 @@ let of_clause ?loc cl = let of_destruction_arg ?loc = function | QElimOnConstr (c, bnd) -> - let c = of_constr ?loc c in + let c = of_open_constr ?loc c in let bnd = of_bindings ?loc bnd in let arg = thunk (of_pair ?loc (c, bnd)) in std_constructor ?loc "ElimOnConstr" [arg] |