aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
-rw-r--r--vernac/comProgramFixpoint.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a6d7fccf3..eef7afbfb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -44,7 +44,7 @@ let mkSubset sigma name typ prop =
let sigT = Lazy.from_fun build_sigma_type
-let make_qref s = CAst.make @@ Qualid (qualid_of_string s)
+let make_qref s = qualid_of_string s
let lt_ref = make_qref "Init.Peano.lt"
let rec telescope sigma l =