fix compilation with old coq

src/coq_elpi_HOAS.ml

@@ -882,24 +882,28 @@ let show_coq_engine ?with_univs e = Format.asprintf "%a" (pp_coq_engine ?with_un
 
  let from_env env = from_env_sigma env (Evd.from_env env)
 
+
+[%%if coq = "8.19" || coq = "8.20"]
+let demote uctx sigma0 env = 
+      let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
+      UState.demote_global_univs env uctx
+[%%else]
+ let demote uctx sigma0 env = 
+  match uctx with
+  | Some x -> UState.demote_global_univs_sound x (Evd.evar_universe_context sigma0)
+  | None ->
+      let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
+      UState.demote_global_univs env uctx
+[%%endif]
+
  let from_env_keep_univ_and_sigma ?uctx ~env0 ~env sigma0 =
    assert(env0 != env);
-   let uctx =
-      match uctx with
-      | Some x -> UState.demote_global_univs_sound x (Evd.evar_universe_context sigma0)
-      | None ->
-          let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
-          UState.demote_global_univs env uctx in
+   let uctx = demote uctx sigma0 env in
    from_env_sigma env (Evd.set_universe_context sigma0 uctx)
 
 let from_env_keep_univ_of_sigma ?uctx ~env0 ~env sigma0 =
    assert(env0 != env);
-   let uctx =
-      match uctx with
-      | Some x -> UState.demote_global_univs_sound x (Evd.evar_universe_context sigma0)
-      | None ->
-          let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
-          UState.demote_global_univs env uctx in
+   let uctx = demote uctx sigma0 env in
    from_env_sigma env (Evd.from_ctx uctx)
 
  let init () =

src/coq_elpi_builtins.ml

@@ -904,8 +904,6 @@ let cinfo_make state types using =
     definition_using (get_global_env state) sigma ~fixnames:[] ~using ~terms:types)
     using in
   Declare.CInfo.make ?using
-let declare_definition _using ~cinfo ~info ~opaque ~body sigma =
-  Declare.declare_definition ~cinfo ~info ~opaque ~body sigma
 let eval_of_constant c =
   match c with
   | Variable v -> Tacred.EvalVarRef v
@@ -926,9 +924,6 @@ let declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_
 
 let cinfo_make _ _ _using =
   Declare.CInfo.make
-let declare_definition using ~cinfo ~info ~opaque ~body sigma =
-  let using = Option.map Proof_using.using_from_string using in
-  Declare.declare_definition ~cinfo ~info ~opaque ~body ?using sigma
 let eval_of_constant c =
   match c with
   | Variable v -> Evaluable.EvalVarRef v
@@ -941,6 +936,22 @@ let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z)
 let pattern_of_glob_constr env g = Patternops.pattern_of_glob_constr env g
 [%%endif]
 
+[%%if coq = "8.19"]
+let declare_definition hack _using ~cinfo ~info ~opaque ~body sigma =
+  let gr = Declare.declare_definition ~cinfo ~info ~opaque ~body sigma in
+  gr, !hack
+[%%elif coq = "8.20"]
+let declare_definition hack using ~cinfo ~info ~opaque ~body sigma =
+  let using = Option.map Proof_using.using_from_string using in
+  let gr = Declare.declare_definition ~cinfo ~info ~opaque ~body ?using sigma in
+  gr, !hack
+[%%else]
+let declare_definition _ using ~cinfo ~info ~opaque ~body sigma =
+  let gr, uctx = Declare.declare_definition ~cinfo ~info ~opaque ~body ?using sigma in
+  gr, Some uctx
+[%%endif]
+
+
 [%%if coq = "8.20"]
 let warns_of_options options = options.user_warns
 [%%elif coq <> "8.19"]
@@ -2001,8 +2012,12 @@ Supported attributes:
         then Locality.Discharge
         else Locality.(Global ImportDefaultBehavior) in
        let cinfo = cinfo_make state types options.using ~name:(Id.of_string id) ~typ:types ~impargs:[] () in
+
+       (* This is a hack, drop after 8.21 *)
        let uctx = ref None in
        let hook = Declare.Hook.make (fun { Declare.Hook.S.uctx = x } -> uctx := Some (UState.context_set x)) in
+       (* End hack *)
+
        let info = Declare.Info.make ~scope ~kind ~poly ~udecl ~hook () in
 
        let used =
@@ -2012,14 +2027,14 @@ Supported attributes:
        let used = Univ.Level.Set.union used (universes_of_udecl state udecl) in
        let sigma = restricted_sigma_of used state in
    
-       let gr = declare_definition options.using ~cinfo ~info ~opaque ~body sigma in
+       let gr, uctx = declare_definition uctx options.using ~cinfo ~info ~opaque ~body sigma in
        let () =
         let lid = CAst.make ~loc:(to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state) (Id.of_string id) in
         match scope with
         | Locality.Discharge -> Dumpglob.dump_definition lid true "var"
         | Locality.Global _ -> Dumpglob.dump_definition lid false "def"
        in
-       !uctx, state, !: (global_constant_of_globref gr), []))),
+       uctx, state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
   MLCode(Pred("coq.env.add-axiom",