From 429da2cda4a507c9ed1e69202af74f705e6a2f49 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 Oct 2024 22:12:49 +0200 Subject: [PATCH] Adapt to Coq PR #19301 which unifies the syntax of Theorem, Definition and Fixpoint --- src/coq_elpi_arg_syntax.mlg | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index 6028ce747..9e7ecc4e3 100644 --- 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 (CList.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 }) }