Merge pull request #718 from SkySkimmer/jump-to-def

gares · web-flow · commit 781859660cc8 · 2024-11-26T18:34:26.000+01:00
Adapt to coq/coq#19584 (record raw ast has loc on idbuild)
diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
@@ -307,7 +307,7 @@ let of_coq_record_definition id =
     name;
     parameters = binders;
     sort;
-    constructor = Some idbuild;
+    constructor = Some idbuild.v;
     fields = cfs;
     univpoly = univpoly_of ~poly ~cumulative
   } 

Original file line number	Diff line number	Diff line change
`@@ -307,7 +307,7 @@ let of_coq_record_definition id =`
`307`	`307`	`name;`
`308`	`308`	`parameters = binders;`
`309`	`309`	`sort;`
`310`		`- constructor = Some idbuild;`
	`310`	`+ constructor = Some idbuild.v;`
`311`	`311`	`fields = cfs;`
`312`	`312`	`univpoly = univpoly_of ~poly ~cumulative`
`313`	`313`	`}`