[declare] Remove trivial wrapper

In preparation for the introduction of an opaque mutual definition
type at the `Declare` level we remove the not very useful wrapper
`declare_fix`.

Now we should be ready to profit from `DeclareDef` and its handling of
common stuff such as `restrict_universe_context` and `check_univ_decl`
etc...

4 files changed, 16 insertions, 33 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a29d60ccde..65dffb3c0b 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -272,8 +272,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   let indexes, cofix, fix_kind =
     match indexes with
-    | Some indexes -> indexes, false, Decls.Fixpoint
-    | None -> [], true, Decls.CoFixpoint
+    | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint)
+    | None -> [], true, Decls.(IsDefinition CoFixpoint)
   in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
@@ -294,11 +294,13 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
   let ctx = Evd.check_univ_decl ~poly evd pl in
-  let pl = Evd.universe_binders evd in
-  let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
-  let fixdecls = List.map mk_pure fixdecls in
-  ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx)
-            fixnames fixdecls fixtypes fiximps);
+  let udecl = Evd.universe_binders evd in
+  let _ : GlobRef.t list =
+    List.map4 (fun name body types imps ->
+        let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
+        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps)
+      fixnames fixdecls fixtypes fiximps
+  in
   recursive_message (not cofix) gidx fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index dea2ccb9af..39fd332184 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,11 +69,6 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   end;
   dref
 
-let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps =
-  let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  let kind = Decls.IsDefinition kind in
-  declare_definition ~name ~scope ~kind ?hook_data udecl ce imps
-
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 17c2862cad..c668ab2ac4 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -49,19 +49,6 @@ val declare_definition
   -> Impargs.manual_implicits
   -> GlobRef.t
 
-val declare_fix
-  :  ?opaque:bool
-  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> name:Id.t
-  -> scope:locality
-  -> kind:Decls.definition_object_kind
-  -> UnivNames.universe_binders
-  -> Entries.universes_entry
-  -> Evd.side_effects Entries.proof_output
-  -> Constr.types
-  -> Impargs.manual_implicits
-  -> GlobRef.t
-
 val declare_assumption
   :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
   -> name:Id.t
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index dcb28b898f..eb9b896ec6 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -376,9 +376,6 @@ let compute_possible_guardness_evidences n fixbody fixtype =
     let ctx = fst (Term.decompose_prod_n_assum m fixtype) in
     List.map_i (fun i _ -> i) 0 ctx
 
-let mk_proof c =
-  ((c, Univ.ContextSet.empty), Evd.empty_side_effects)
-
 let declare_mutual_definition l =
   let len = List.length l in
   let first = List.hd l in
@@ -410,7 +407,6 @@ let declare_mutual_definition l =
   let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
   let fixnames = first.prg_deps in
   let opaque = first.prg_opaque in
-  let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
     | IsFixpoint wfl ->
@@ -421,20 +417,23 @@ let declare_mutual_definition l =
         Pretyping.search_guard (Global.env ()) possible_indexes fixdecls
       in
       ( Some indexes
-      , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l
+      , List.map_i (fun i _ -> mkFix ((indexes, i), fixdecls)) 0 l
       )
     | IsCoFixpoint ->
-      (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l)
+      (None, List.map_i (fun i _ -> mkCoFix (i, fixdecls)) 0 l)
   in
   (* Declare the recursive definitions *)
   let poly = first.prg_poly in
   let scope = first.prg_scope in
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
+  let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
+  let udecl = UnivNames.empty_binders in
   let kns =
     List.map4
-      (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind
-          UnivNames.empty_binders univs)
+      (fun name body types imps ->
+         let ce = Declare.definition_entry ~opaque ~types ~univs body in
+         DeclareDef.declare_definition ~name ~scope ~kind udecl ce imps)
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)