Merge pull request #680 from SkySkimmer/redbehaviour-pred

coq · Oct 26, 2023 · e2ac4a9 · e2ac4a9
2 parents d2b3249 + b3a7ed9
commit e2ac4a9
Showing 1 changed file with 10 additions and 6 deletions.
diff --git a/language-server/language/hover.ml b/language-server/language/hover.ml
@@ -169,11 +169,15 @@ let rec insert_fake_args volatile bidi impls =
 let print_arguments ref =
   let flags, recargs, nargs_for_red =
     let open Reductionops.ReductionBehaviour in
-    match get ref with
-    | None -> [], [], None
-    | Some NeverUnfold -> [`ReductionNeverUnfold], [], None
-    | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
-    | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
+    match ref with
+    | GlobRef.ConstRef ref ->
+      begin match get ref with
+      | None -> [], [], None
+      | Some NeverUnfold -> [`ReductionNeverUnfold], [], None
+      | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
+      | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
+      end
+    | _ -> [], [], None
   in
   let names, not_renamed =
     try Arguments_renaming.arguments_names ref, false
@@ -260,4 +264,4 @@ let get_hover_contents env sigma ref_or_by_not =
     end
     in
     Option.map Lsp.Types.(fun value -> MarkupContent.create ~kind:MarkupKind.Markdown ~value) r
-  | Constrexpr.ByNotation (_ntn,_sc) -> assert false
+  | Constrexpr.ByNotation (_ntn,_sc) -> assert false