Adapt to Coq PR #19301 which unifies the syntax of Theorem, Definitio…

…n and Fixpoint
LPCIC · Oct 24, 2024 · 92e0803 · 92e0803
1 parent c7fcee1
commit 92e0803
Showing 1 changed file with 17 additions and 4 deletions.
diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg
@@ -181,6 +181,8 @@ let pr_attributes _ _ _ atts =
 
 let wit_elpi_ftactic_arg = EA.Tac.wit
 
+let binders = Pcoq.Constr.binders
+
 let def_body = G_vernac.def_body
 
 let of_coq_inductive_declaration ~atts kind id =
@@ -195,12 +197,23 @@ let of_coq_record_declaration ~atts kind id =
   | Inductive _ -> assert false
   | Record r -> r
 
-let of_coq_definition ~loc ~atts name udecl def =
+[%%if coq = "8.20"]
+let of_coq_definition ~loc ~atts name udecl bl def =
+  match def with
+  | Vernacexpr.DefineBody(bl',red,c,ty) ->
+      (* For compatibility with Coq PR #19301, binders have been parsed in advance *)
+      assert (List.is_empty bl');
+      EA.Cmd.(ConstantDecl { name = snd name; atts; udecl; typ = (bl,ty); red; body = Some c })
+  | Vernacexpr.ProveBody _ ->
+      CErrors.user_err ~loc Pp.(str"syntax error: missing Definition body")
+[%%else]
+let of_coq_definition ~loc ~atts name udecl bl def =
   match def with
-  | Vernacexpr.DefineBody(bl,red,c,ty) ->
+  | Vernacexpr.DefineBody(red,c,ty) ->
       EA.Cmd.(ConstantDecl { name = snd name; atts; udecl; typ = (bl,ty); red; body = Some c })
   | Vernacexpr.ProveBody _ ->
       CErrors.user_err ~loc Pp.(str"syntax error: missing Definition body")
+[%%endif]
 
 }
 
@@ -285,8 +298,8 @@ GLOB_PRINTED BY { fun _ _ _ -> EA.Cmd.pp_glob env sigma }
 | [ "Structure" inductive_or_record_definition(id) ] -> { EA.Cmd.RecordDecl (of_coq_record_declaration ~atts:[] Vernacexpr.Structure id) }  
 | [ "#[" attributes(atts) "]" "Structure" inductive_or_record_definition(id) ] -> { EA.Cmd.RecordDecl (of_coq_record_declaration ~atts Vernacexpr.Structure id) }  
 
-| [ "Definition" qualified_name(name) univ_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts:[] name udecl def }
-| [ "#[" attributes(atts) "]" "Definition" qualified_name(name) univ_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts name udecl def }
+| [ "Definition" qualified_name(name) univ_decl_opt(udecl) binders(bl) def_body(def) ] -> { of_coq_definition ~loc ~atts:[] name udecl bl def }
+| [ "#[" attributes(atts) "]" "Definition" qualified_name(name) univ_decl_opt(udecl) binders(bl) def_body(def) ] -> { of_coq_definition ~loc ~atts name udecl bl def }
 
 | [ "Axiom" qualified_name(name) univ_decl_opt(udecl) telescope(typ) colon_constr(t) ] -> {
       EA.Cmd.(ConstantDecl { name = snd name; atts = []; udecl; typ = (typ,Some t); red = None; body = None }) }