[declare] More uniformity in arguments labels / names

In anticipation for more consolidation of duplicated functionality.

5 files changed, 27 insertions, 26 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 29f5355fce..dafd1cc5e4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
   instance_hook pri global impargs (GlobRef.ConstRef cst)
 
-let declare_instance_program env sigma ~global ~poly name pri imps univdecl term termtype =
+let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype =
   let hook { DeclareDef.Hook.S.scope; dref; _ } =
     let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
     Impargs.declare_manual_implicits false dref imps;
@@ -345,10 +345,10 @@ let declare_instance_program env sigma ~global ~poly name pri imps univdecl term
   in
   let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in
   let hook = DeclareDef.Hook.make hook in
-  let ctx = Evd.evar_universe_context sigma in
+  let uctx = Evd.evar_universe_context sigma in
   let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in
   let _ : DeclareObl.progress =
-    Obligations.add_definition ~name ~term ~univdecl ~scope ~poly ~kind ~hook typ ctx obls
+    Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls
   in ()
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 26592b5542..ba2c1ac115 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -79,9 +79,9 @@ let check_definition ~program_mode (ce, evd, _, imps) =
   check_evars_are_solved ~program_mode env evd;
   ce
 
-let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt =
-  let (ce, evd, univdecl, impargs as def) =
-    interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt
+let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+  let (ce, evd, udecl, impargs as def) =
+    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
   if program_mode then
     let env = Global.env () in
@@ -97,9 +97,9 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
     let obls, _, c, cty =
       Obligations.eterm_obligations env name evd 0 c typ
     in
-    let ctx = Evd.evar_universe_context evd in
+    let uctx = Evd.evar_universe_context evd in
     ignore(Obligations.add_definition
-             ~name ~term:c cty ctx ~univdecl ~implicits:impargs ~scope ~poly ~kind ?hook obls)
+             ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls)
   else
     let ce = check_definition ~program_mode def in
     let uctx = Evd.evar_universe_context evd in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 4f9c247b71..3bac0419ef 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -115,7 +115,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
+  let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -234,7 +234,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
         let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
         let ty = EConstr.Unsafe.to_constr ty in
-        let univs = Evd.check_univ_decl ~poly sigma decl in
+        let univs = Evd.check_univ_decl ~poly sigma udecl in
         (*FIXME poly? *)
         let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
         (* FIXME: include locality *)
@@ -258,9 +258,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let evars, _, evars_def, evars_typ =
     Obligations.eterm_obligations env recname sigma 0 def typ
   in
-  let ctx = Evd.evar_universe_context sigma in
-    ignore(Obligations.add_definition ~name:recname ~term:evars_def ~univdecl:decl
-             ~poly evars_typ ctx evars ~hook)
+  let uctx = Evd.evar_universe_context sigma in
+  ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
+           ~poly evars_typ ~uctx evars ~hook)
 
 let out_def = function
   | Some def -> def
@@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty =
 
 let do_program_recursive ~scope ~poly fixkind fixl =
   let cofix = fixkind = DeclareObl.IsCoFixpoint in
-  let (env, rec_sign, pl, evd), fix, info =
+  let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
   in
     (* Program-specific code *)
@@ -311,13 +311,13 @@ let do_program_recursive ~scope ~poly fixkind fixl =
                               ((indexes,i),fixdecls))
         fixl
   end in
-  let ctx = Evd.evar_universe_context evd in
+  let uctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
   | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
   | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
-  Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind
 
 let do_fixpoint ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index d6ce1036b9..b38c23631f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -630,11 +630,11 @@ let show_term n =
              Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
-let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
-                   ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
+let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
+                   ?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let info = Id.print name ++ str " has type-checked" in
-  let prg = init_prog_info ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in
+  let prg = init_prog_info ~opaque name udecl term t uctx [] None [] obls impargs ~poly ~scope ~kind reduce ?hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -649,13 +649,13 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
         | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res
         | _ -> res)
 
-let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
+let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
                            ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info ~opaque n udecl (Some b) t uctx deps (Some fixkind)
        notations obls imps ~poly ~scope ~kind reduce ?hook
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 6a2eb1472e..101958072a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -51,9 +51,9 @@ val default_tactic : unit Proofview.tactic ref
 val add_definition
   :  name:Names.Id.t
   -> ?term:constr -> types
-  -> UState.t
-  -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
-  -> ?implicits:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> ?udecl:UState.universe_decl (* Universe binders and constraints *)
+  -> ?impargs:Impargs.manual_implicits
   -> poly:bool
   -> ?scope:DeclareDef.locality
   -> ?kind:Decls.definition_object_kind
@@ -65,9 +65,10 @@ val add_definition
   -> DeclareObl.progress
 
 val add_mutual_definitions
+  (* XXX: unify with MutualEntry *)
   : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list
-  -> UState.t
-  -> ?univdecl:UState.universe_decl
+  -> uctx:UState.t
+  -> ?udecl:UState.universe_decl
   (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
   -> poly:bool