Adapt to Coq PR #19301: unify the syntax of definition and theorem

In particular, VernacStartTheoremProof and VernacDefinition are merged.
coq · Oct 23, 2024 · f5c98e4 · f5c98e4
1 parent 50b41ad
commit f5c98e4
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
@@ -122,8 +122,8 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
       | VernacSynterp _ -> None, ""
       | VernacSynPure pure -> 
         match pure with
-        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), "theorem"
-        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), "definition"
+        | Vernacexpr.VernacDefinition ((_, IsTheoremKind kind), _) -> Some (TheoremKind kind), "theorem"
+        | Vernacexpr.VernacDefinition ((_, IsDefinitionKind def), _) -> Some (DefinitionType def), "definition"
         | _ -> None, ""
     in
     let name = match names with
@@ -144,8 +144,8 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
       | VernacSynterp _ -> None, ""
       | VernacSynPure pure -> 
         match pure with
-        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), "theroem"
-        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), "definition"
+        | Vernacexpr.VernacDefinition ((_, IsTheoremKind kind), _) -> Some (TheoremKind kind), "theroem"
+        | Vernacexpr.VernacDefinition ((_, IsDefinitionKind def), _) -> Some (DefinitionType def), "definition"
         | _ -> None, ""
     in
     let name = match names with