Merge pull request #722 from ppedrot/prettyp-explicit-env

coq · Feb 19, 2024 · 50231cb · 50231cb
2 parents 6036251 + 3166634
commit 50231cb
Showing 1 changed file with 12 additions and 6 deletions.
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
@@ -452,14 +452,20 @@ let check st pos ~pattern =
       let e, info = Exninfo.capture e in
       Error (Pp.string_of_ppcmds @@ CErrors.iprint (e, info))
 
+[%%if coq = "8.18" || coq = "8.19"]
+let print_located_qualid _ qid = Prettyp.print_located_qualid qid
+[%%else]
+let print_located_qualid = Prettyp.print_located_qualid
+[%%endif]
+
 let locate st pos ~pattern = 
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
-  match parse_entry st loc (Pcoq.Prim.smart_global) pattern with
-  | { v = AN qid } -> Ok (pp_of_coqpp @@ Prettyp.print_located_qualid qid)
-  | { v = ByNotation (ntn, sc)} -> 
-    match get_context st pos with
-    | None -> Error("No context found")
-    | Some (sigma, env) -> 
+  match get_context st pos with
+  | None -> Error ("No context found") (*TODO execute *)
+  | Some (sigma, env) ->
+    match parse_entry st loc (Pcoq.Prim.smart_global) pattern with
+    | { v = AN qid } -> Ok (pp_of_coqpp @@ print_located_qualid env qid)
+    | { v = ByNotation (ntn, sc)} ->
       Ok( pp_of_coqpp @@ Notation.locate_notation
         (Constrextern.without_symbols (Printer.pr_glob_constr_env env sigma)) ntn sc)