aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/g_obligations.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/g_obligations.ml4')
-rw-r--r--plugins/ltac/g_obligations.ml45
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 352e92c2a..1f56244c7 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,6 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe FilliĆ¢tre *)
-open Libnames
open Constrexpr
open Constrexpr_ops
open Stdarg
@@ -49,7 +48,7 @@ module Tactic = Pltac
open Pcoq
-let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig")
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
@@ -68,7 +67,7 @@ GEXTEND Gram
Constr.closed_binder:
[[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
- let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+ let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in
[CLocalAssum ([id], default_binder_kind, typ)]
] ];