More precise type for quoted structures.

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]