adapt to rocq 9.1

Author: gares

src/rocq_elpi_builtins.ml

@@ -1562,6 +1562,19 @@ let apply_proof ~name ~poly env tac pf =
 [%%endif]
 
 
+[%%if coq = "9.0"]
+let section_close_section x =
+  let a,b,_,_ = Section.close_section x in
+  a, b
+[%%elif coq = "9.1"]
+let section_close_section x =
+  let a,b,_ = Section.close_section x in
+  a, b
+[%%else]
+let section_close_section x =
+  let a,b,_,_ = Section.close_section x in
+  a, b
+[%%endif]
 
 
 
@@ -2154,7 +2167,7 @@ Supported attributes:
         match section with
         | None -> []
         | Some s ->
-            let section,l,_,_ = Section.close_section s in
+            let section,l = section_close_section s in
             List.concat_map (function
               | Section.SecDefinition c -> [GlobRef.ConstRef c]
               | Section.SecInductive m ->