[vernac] more precise types for Add Morph, Instance, and Function

7 files changed, 411 insertions, 243 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index bb6db1f5cf..241da053b7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-      let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in
+       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
@@ -448,7 +448,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
-       pstate,evd,List.rev rev_pconstants
+       None,evd,List.rev rev_pconstants
 
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c568f63903..caeedadbf4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1796,11 +1796,11 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance atts binders (name,t) fields =
   let program_mode = atts.program in
-  let _id, proof = Classes.new_instance ~program_mode atts.polymorphic
-      name binders t (Some (true, CAst.make @@ CRecord (fields)))
+  let _id = Classes.new_instance ~program_mode atts.polymorphic
+      name binders t (true, CAst.make @@ CRecord (fields))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
-  assert (Option.is_empty proof) (* refine:false with term *)
+  ()
 
 let declare_instance_refl atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
@@ -2024,12 +2024,12 @@ let add_morphism atts binders m s n =
        [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let _, pstate = Classes.new_instance
+  let _id, pstate = Classes.new_instance_interactive
       ~program_mode:atts.program ~global:atts.global atts.polymorphic
-      instance_name binders instance_t None
+      instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
-  Option.get pstate (* no instance body -> always open proof *)
+  pstate (* no instance body -> always open proof *)
 
 (** Bind to "rewrite" too *)
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b9f57c0727..2ef30e770c 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -404,75 +404,18 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
   | None ->
     pstate
 
-let do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
-  let props =
-    match props with
-    | Some (true, { CAst.v = CRecord fs }) ->
-      if List.length fs > List.length k.cl_props then
-        mismatched_props env' (List.map snd fs) k.cl_props;
-      Some (Inl fs)
-    | Some (_, t) -> Some (Inr t)
-    | None ->
-      if program_mode then Some (Inl [])
-      else None
-  in
-  let subst, sigma =
-    match props with
-    | None ->
-      (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
-    | Some (Inr term) ->
-      let sigma, c = interp_casted_constr_evars ~program_mode env' sigma term cty in
-      Some (Inr (c, subst)), sigma
-    | Some (Inl props) ->
-      let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
-      let props, rest =
-        List.fold_left
-          (fun (props, rest) decl ->
-             if is_local_assum decl then
-               try
-                 let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
-                   | Name id, {CAst.v=id'} -> Id.equal id id'
-                   | Anonymous, _ -> false
-                 in
-                 let (loc_mid, c) = List.find is_id rest in
-                 let rest' = List.filter (fun v -> not (is_id v)) rest
-                 in
-                 let {CAst.loc;v=mid} = get_id loc_mid in
-                 List.iter (fun (n, _, x) ->
-                     if Name.equal n (Name mid) then
-                       Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs;
-                 c :: props, rest'
-               with Not_found ->
-                 ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
-             else props, rest)
-          ([], props) k.cl_props
-      in
-      match rest with
-      | (n, _) :: _ ->
-        unbound_method env' sigma k.cl_impl (get_id n)
-      | _ ->
-        let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
-        let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
-        Some (Inl res), sigma
-  in
-  let term, termtype =
-    match subst with
-    | None -> let termtype = it_mkProd_or_LetIn cty ctx in
-      None, termtype
-    | Some (Inl subst) ->
-      let subst = List.fold_left2
-          (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
-          [] subst (k.cl_props @ snd k.cl_context)
-      in
-      let (app, ty_constr) = instance_constructor (k,u) subst in
-      let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-      let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
-      Some term, termtype
-    | Some (Inr (def, subst)) ->
-      let termtype = it_mkProd_or_LetIn cty ctx in
-      let term = it_mkLambda_or_LetIn def ctx in
-      Some term, termtype
+let do_instance_subst_constructor_and_ty subst k u ctx =
+  let subst =
+    List.fold_left2 (fun subst' s decl ->
+      if is_local_assum decl then s :: subst' else subst')
+    [] subst (k.cl_props @ snd k.cl_context)
   in
+  let (app, ty_constr) = instance_constructor (k,u) subst in
+  let termtype = it_mkProd_or_LetIn ty_constr ctx in
+  let term = it_mkLambda_or_LetIn (Option.get app) ctx in
+  term, termtype
+
+let do_instance_resolve_TC term termtype sigma env =
   let sigma = Evarutil.nf_evar_map sigma in
   let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in
   (* Try resolving fields that are typeclasses automatically. *)
@@ -483,24 +426,108 @@ let do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ct
   (* Check that the type is free of evars now. *)
   Pretyping.check_evars env (Evd.from_env env) sigma termtype;
   let termtype = to_constr sigma termtype in
-  let pstate =
-    if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
-      let term = to_constr sigma (Option.get term) in
-      (declare_instance_constant pri global imps ?hook id decl poly sigma term termtype;
-       None)
-    else if program_mode then
-      (declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype;
-       None)
-    else if Option.is_empty props then
-      let pstate =
-        Flags.silently (fun () ->
-            declare_instance_open sigma ?hook ~tac ~global ~poly
-              id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
-          ()
-      in
-      Some pstate
-    else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
-  id, pstate
+  termtype, sigma
+
+let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
+  let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
+  let props, rest =
+    List.fold_left
+      (fun (props, rest) decl ->
+         if is_local_assum decl then
+           try
+             let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
+               | Name id, {CAst.v=id'} -> Id.equal id id'
+               | Anonymous, _ -> false
+             in
+             let (loc_mid, c) = List.find is_id rest in
+             let rest' = List.filter (fun v -> not (is_id v)) rest
+             in
+             let {CAst.loc;v=mid} = get_id loc_mid in
+             List.iter (fun (n, _, x) ->
+                 if Name.equal n (Name mid) then
+                   Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs;
+             c :: props, rest'
+           with Not_found ->
+             ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
+         else props, rest)
+      ([], props) k.cl_props
+  in
+  match rest with
+  | (n, _) :: _ ->
+    unbound_method env' sigma k.cl_impl (get_id n)
+  | _ ->
+    let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
+    let sigma, res =
+      type_ctx_instance ~program_mode
+        (push_rel_context ctx' env') sigma kcl_props props subst in
+    res, sigma
+
+let do_instance_interactive env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id =
+  let term, termtype =
+    if List.is_empty k.cl_props then
+     let term, termtype =
+       do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+     Some term, termtype
+    else
+      None, it_mkProd_or_LetIn cty ctx in
+  let termtype, sigma = do_instance_resolve_TC term termtype sigma env in
+  Flags.silently (fun () ->
+      declare_instance_open sigma ?hook ~tac ~global ~poly
+        id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
+    ()
+
+let do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+  let term, termtype, sigma =
+    match props with
+    | (true, { CAst.v = CRecord fs }) ->
+      if List.length fs > List.length k.cl_props then
+        mismatched_props env' (List.map snd fs) k.cl_props;
+      let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in
+      let term, termtype =
+        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+      term, termtype, sigma
+    | (_, term) ->
+      let sigma, def =
+        interp_casted_constr_evars ~program_mode env' sigma term cty in
+      let termtype = it_mkProd_or_LetIn cty ctx in
+      let term = it_mkLambda_or_LetIn def ctx in
+      term, termtype, sigma in
+  let termtype, sigma = do_instance_resolve_TC (Some term) termtype sigma env in
+  if Evd.has_undefined sigma then
+    CErrors.user_err Pp.(str "Unsolved obligations remaining.")
+  else
+    let term = to_constr sigma term in
+    declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
+
+let do_instance_program env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id opt_props =
+  let term, termtype, sigma =
+    match opt_props with
+    | Some (true, { CAst.v = CRecord fs }) ->
+      if List.length fs > List.length k.cl_props then
+        mismatched_props env' (List.map snd fs) k.cl_props;
+      let subst, sigma =
+        do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in
+     let term, termtype =
+       do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+     Some term, termtype, sigma
+    | Some (_, term) ->
+      let sigma, def =
+        interp_casted_constr_evars ~program_mode env' sigma term cty in
+      let termtype = it_mkProd_or_LetIn cty ctx in
+      let term = it_mkLambda_or_LetIn def ctx in
+      Some term, termtype, sigma
+    | None ->
+      let subst, sigma =
+        do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode subst in
+      let term, termtype =
+        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+      Some term, termtype, sigma in
+  let termtype, sigma = do_instance_resolve_TC term termtype sigma env in
+  if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then
+    let term = to_constr sigma (Option.get term) in
+    declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
+  else
+    declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype
 
 let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -530,14 +557,12 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass
   let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
   sigma, cl, u, c', ctx', ctx, imps, args, decl
 
-let new_instance ?(global=false) ~program_mode
-    poly instid ctx cl props
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
-  let env = Global.env() in
+let new_instance_common ~program_mode ~generalize env instid ctx cl =
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
     interp_instance_context ~program_mode env ~generalize ctx pl cl
   in
+  (* The name generator should not be here *)
   let id =
     match instid with
     | Name id -> id
@@ -546,8 +571,36 @@ let new_instance ?(global=false) ~program_mode
       Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
+  id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl
+
+let new_instance_interactive ?(global=false) ~program_mode
+    poly instid ctx cl
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+  let env = Global.env() in
+  let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    new_instance_common ~program_mode ~generalize env instid ctx cl in
+  id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly ~program_mode
+    cty k u ctx ctx' pri decl imps subst id
+
+let new_instance_program ?(global=false) ~program_mode
+    poly instid ctx cl opt_props
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+  let env = Global.env() in
+  let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    new_instance_common ~program_mode ~generalize env instid ctx cl in
+  do_instance_program env env' sigma ?hook ~tac ~global ~poly ~program_mode
+    cty k u ctx ctx' pri decl imps subst id opt_props;
+  id
+
+let new_instance ?(global=false) ~program_mode
+    poly instid ctx cl props
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+  let env = Global.env() in
+  let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    new_instance_common ~program_mode ~generalize env instid ctx cl in
   do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode
-    cty k u ctx ctx' pri decl imps subst id props
+    cty k u ctx ctx' pri decl imps subst id props;
+  id
 
 let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri =
   let env = Global.env() in
diff --git a/vernac/classes.mli b/vernac/classes.mli
index daba78217b..9572cd9598 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -31,6 +31,19 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
 val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
+val new_instance_interactive :
+  ?global:bool (** Not global by default. *)
+  -> program_mode:bool
+  -> Decl_kinds.polymorphic
+  -> name_decl
+  -> local_binder_expr list
+  -> constr_expr
+  -> ?generalize:bool
+  -> ?tac:unit Proofview.tactic
+  -> ?hook:(GlobRef.t -> unit)
+  -> Hints.hint_info_expr
+  -> Id.t * Proof_global.t
+
 val new_instance :
   ?global:bool (** Not global by default. *)
   -> program_mode:bool
@@ -38,12 +51,26 @@ val new_instance :
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
+  -> (bool * constr_expr)
+  -> ?generalize:bool
+  -> ?tac:unit Proofview.tactic
+  -> ?hook:(GlobRef.t -> unit)
+  -> Hints.hint_info_expr
+  -> Id.t
+
+val new_instance_program :
+  ?global:bool (** Not global by default. *)
+  -> program_mode:bool
+  -> Decl_kinds.polymorphic
+  -> name_decl
+  -> local_binder_expr list
+  -> constr_expr
   -> (bool * constr_expr) option
   -> ?generalize:bool
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
-  -> Id.t * Proof_global.t option (* May open a proof *)
+  -> Id.t
 
 val declare_new_instance
   : ?global:bool (** Not global by default. *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 006ac314a5..7a4e6d8698 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,79 +255,78 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
+let declare_fixpoint_notations ntns =
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+
+let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+  (* Some bodies to define by proof *)
+  let thms =
+    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
+              fixnames fixtypes fiximps in
+  let init_tac =
+    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
+      fixdefs) in
+  let evd = Evd.from_ctx ctx in
+  let pstate = Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
+    evd pl (Some(false,indexes,init_tac)) thms None in
+  declare_fixpoint_notations ntns;
+  pstate
+
 let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
-  let pstate =
-  if List.exists Option.is_empty fixdefs then
-    (* Some bodies to define by proof *)
-    let thms =
-      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-                fixnames fixtypes fiximps in
-    let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
-        fixdefs) in
-    let evd = Evd.from_ctx ctx in
-    Some
-    (Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
-      evd pl (Some(false,indexes,init_tac)) thms None)
-  else begin
-    (* We shortcut the proof process *)
-    let fixdefs = List.map Option.get fixdefs in
-    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-    let env = Global.env() in
-    let indexes = search_guard env indexes fixdecls in
-    let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
-    let fixdecls =
-      List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    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 fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
-              fixnames fixdecls fixtypes fiximps);
-    (* Declare the recursive definitions *)
-    fixpoint_message (Some indexes) fixnames;
-    None
-  end in
-  (* Declare notations *)
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+  (* We shortcut the proof process *)
+  let fixdefs = List.map Option.get fixdefs in
+  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
+  let env = Global.env() in
+  let indexes = search_guard env indexes fixdecls in
+  let fiximps = List.map (fun (n,r,p) -> r) fiximps in
+  let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+  let fixdecls =
+    List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+  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 fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+  ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
+            fixnames fixdecls fixtypes fiximps);
+  (* Declare the recursive definitions *)
+  fixpoint_message (Some indexes) fixnames;
+  declare_fixpoint_notations ntns
+
+let declare_cofixpoint_notations = declare_fixpoint_notations
+
+let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+  (* Some bodies to define by proof *)
+  let thms =
+    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
+              fixnames fixtypes fiximps in
+  let init_tac =
+    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
+      fixdefs) in
+  let evd = Evd.from_ctx ctx in
+  let pstate = Lemmas.start_proof_with_initialization
+    (Global,poly, DefinitionBody CoFixpoint)
+    evd pl (Some(true,[],init_tac)) thms None in
+  declare_cofixpoint_notations ntns;
   pstate
 
 let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  let pstate =
-  if List.exists Option.is_empty fixdefs then
-    (* Some bodies to define by proof *)
-    let thms =
-      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-                fixnames fixtypes fiximps in
-    let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
-        fixdefs) in
-    let evd = Evd.from_ctx ctx in
-    Some (Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-            evd pl (Some(true,[],init_tac)) thms None)
-  else begin
-    (* We shortcut the proof process *)
-    let fixdefs = List.map Option.get fixdefs in
-    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-    let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let vars = Vars.universes_of_constr (List.hd fixdecls) in
-    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    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
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
-              fixnames fixdecls fixtypes fiximps);
-    (* Declare the recursive definitions *)
-    cofixpoint_message fixnames;
-    None
-  end in
-  (* Declare notations *)
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
-  pstate
+  (* We shortcut the proof process *)
+  let fixdefs = List.map Option.get fixdefs in
+  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
+  let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+  let vars = Vars.universes_of_constr (List.hd fixdecls) in
+  let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+  let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
+  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
+  ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+            fixnames fixdecls fixtypes fiximps);
+  (* Declare the recursive definitions *)
+  cofixpoint_message fixnames;
+  declare_cofixpoint_notations ntns
 
 let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
   | CStructRec na -> na
@@ -366,18 +365,33 @@ let check_safe () =
   let flags = Environ.typing_flags (Global.env ()) in
   flags.check_universes && flags.check_guarded
 
-let do_fixpoint local poly l =
+let do_fixpoint_common l =
   let fixl, ntns = extract_fixpoint_components ~structonly:true l in
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
-  let possible_indexes =
-    List.map compute_possible_guardness_evidences info in
-  let pstate = declare_fixpoint local poly fix possible_indexes ntns in
+  fixl, ntns, fix, List.map compute_possible_guardness_evidences info
+
+let do_fixpoint_interactive local poly l =
+  let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
+  let pstate = declare_fixpoint_interactive local poly fix possible_indexes ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   pstate
 
-let do_cofixpoint local poly l =
+let do_fixpoint local poly l =
+  let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
+  declare_fixpoint local poly fix possible_indexes ntns;
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+
+let do_cofixpoint_common l =
   let fixl,ntns = extract_cofixpoint_components l in
-  let cofix = interp_fixpoint ~cofix:true fixl ntns in
-  let pstate = declare_cofixpoint local poly cofix ntns in
+  ntns, interp_fixpoint ~cofix:true fixl ntns
+
+let do_cofixpoint_interactive local poly l =
+  let ntns, cofix = do_cofixpoint_common l in
+  let pstate = declare_cofixpoint_interactive local poly cofix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   pstate
+
+let do_cofixpoint local poly l =
+  let ntns, cofix = do_cofixpoint_common l in
+  declare_cofixpoint local poly cofix ntns;
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 9e376c8f96..b32ea44da2 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -18,13 +18,21 @@ open Vernacexpr
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
+val do_fixpoint_interactive :
+  (* When [false], assume guarded. *)
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t
+
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+
+val do_cofixpoint_interactive :
+  (* When [false], assume guarded. *)
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (************************************************************************)
 (** Internal API  *)
@@ -84,15 +92,13 @@ val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  Proof_global.lemma_possible_guards -> decl_notation list ->
-  Proof_global.t option
+  Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  decl_notation list ->
-  Proof_global.t option
+  decl_notation list -> unit
 
 (** Very private function, do not use *)
 val compute_possible_guardness_evidences :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index da9fa35202..9859bb62f0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -581,47 +581,48 @@ let vernac_definition_hook p = function
   Some (Class.add_subclass_hook p)
 | _ -> None
 
-let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def ~pstate =
+let vernac_definition_name lid local ~pstate =
+  let lid =
+    match lid with
+    | { v = Name.Anonymous; loc } -> CAst.make ?loc (fresh_name_for_anonymous_theorem ~pstate)
+    | { v = Name.Name n; loc } -> CAst.make ?loc n in
+  let () =
+    match local with
+    | Discharge -> Dumpglob.dump_definition lid true "var"
+    | Local | Global -> Dumpglob.dump_definition lid false "def"
+  in
+  lid
+
+let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t ~pstate =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
-  let () =
-    match id with
-    | Anonymous -> ()
-    | Name n -> let lid = CAst.make ?loc n in
-      match local with
-      | Discharge -> Dumpglob.dump_definition lid true "var"
-      | Local | Global -> Dumpglob.dump_definition lid false "def"
-  in
   let program_mode = atts.program in
-  let name =
-    match id with
-    | Anonymous -> fresh_name_for_anonymous_theorem ~pstate
-    | Name n -> n
-  in
-  (match def with
-    | ProveBody (bl,t) ->   (* local binders, typ *)
-      Some (start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind)
-              ?hook [(CAst.make ?loc name, pl), (bl, t)])
-    | DefineBody (bl,red_option,c,typ_opt) ->
-      let pstate = Option.map Proof_global.get_current_pstate pstate in
-      let red_option = match red_option with
-        | None -> None
-        | Some r ->
-          let sigma, env = get_current_or_global_context ~pstate in
-          Some (snd (Hook.get f_interp_redexp env sigma r)) in
-      ComDefinition.do_definition ~program_mode name
-        (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
-      None
-  )
+  let name = vernac_definition_name lid local ~pstate in
+  start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
+
+let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt ~pstate =
+  let open DefAttributes in
+  let local = enforce_locality_exp atts.locality discharge in
+  let hook = vernac_definition_hook atts.polymorphic kind in
+  let program_mode = atts.program in
+  let name = vernac_definition_name lid local ~pstate in
+  let pstate = Option.map Proof_global.get_current_pstate pstate in
+  let red_option = match red_option with
+    | None -> None
+    | Some r ->
+      let sigma, env = get_current_or_global_context ~pstate in
+      Some (snd (Hook.get f_interp_redexp env sigma r)) in
+  ComDefinition.do_definition ~program_mode name.v
+    (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook
 
 (* NB: pstate argument to use combinators easily *)
-let vernac_start_proof ~atts kind l ~pstate =
+let vernac_start_proof ~atts kind l =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  Some (start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
+  start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
 
 let vernac_end_proof ?pstate:ontop ?proof = function
   | Admitted ->
@@ -814,30 +815,46 @@ let vernac_inductive ~atts cum lo finite indl =
       in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
     *)
 
-let vernac_fixpoint ~atts discharge l ~pstate =
-  let open DefAttributes in
-  let local = enforce_locality_exp atts.locality discharge in
+let vernac_fixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  (* XXX: Switch to the attribute system and match on ~atts *)
-  let do_fixpoint = if atts.program then
-      fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None
-    else
-      ComFixpoint.do_fixpoint
-  in
-  do_fixpoint local atts.polymorphic l
+  enforce_locality_exp atts.DefAttributes.locality discharge
 
-let vernac_cofixpoint ~atts discharge l ~pstate =
+let vernac_fixpoint_interactive ~atts discharge l =
   let open DefAttributes in
-  let local = enforce_locality_exp atts.locality discharge in
+  let local = vernac_fixpoint_common ~atts discharge l in
+  if atts.program then
+    CErrors.user_err Pp.(str"Program Fixpoint requires a body");
+  ComFixpoint.do_fixpoint_interactive local atts.polymorphic l
+
+let vernac_fixpoint ~atts discharge l =
+  let open DefAttributes in
+  let local = vernac_fixpoint_common ~atts discharge l in
+  if atts.program then
+    (* XXX: Switch to the attribute system and match on ~atts *)
+    ComProgramFixpoint.do_fixpoint local atts.polymorphic l
+  else
+    ComFixpoint.do_fixpoint local atts.polymorphic l
+
+let vernac_cofixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  let do_cofixpoint = if atts.program then
-      fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None
-    else
-      ComFixpoint.do_cofixpoint
-  in
-  do_cofixpoint local atts.polymorphic l
+  enforce_locality_exp atts.DefAttributes.locality discharge
+
+let vernac_cofixpoint_interactive ~atts discharge l =
+  let open DefAttributes in
+  let local = vernac_cofixpoint_common ~atts discharge l in
+  if atts.program then
+    CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
+  ComFixpoint.do_cofixpoint_interactive local atts.polymorphic l
+
+let vernac_cofixpoint ~atts discharge l =
+  let open DefAttributes in
+  let local = vernac_cofixpoint_common ~atts discharge l in
+  if atts.program then
+    ComProgramFixpoint.do_cofixpoint local atts.polymorphic l
+  else
+    ComFixpoint.do_cofixpoint local atts.polymorphic l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1068,12 +1085,35 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance ~atts name bl t props pri =
+let vernac_instance_common ~atts name =
   let open DefAttributes in
   let global = not (make_section_locality atts.locality) in
   Dumpglob.dump_constraint (fst name) false "inst";
   let program_mode = atts.program in
-  Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri
+  program_mode, global
+
+let vernac_instance_interactive ~atts name bl t pri =
+  let open DefAttributes in
+  let program_mode, global = vernac_instance_common ~atts name in
+  let _id, pstate =
+    Classes.new_instance_interactive
+      ~program_mode ~global atts.polymorphic name bl t pri in
+  pstate
+
+let vernac_instance_program ~atts name bl t opt_props pri =
+  let open DefAttributes in
+  let program_mode, global = vernac_instance_common ~atts name in
+  let _id = Classes.new_instance_program
+    ~program_mode ~global atts.polymorphic name bl t opt_props pri in
+  ()
+
+let vernac_instance ~atts name bl t props pri =
+  let open DefAttributes in
+  let program_mode, global = vernac_instance_common ~atts name in
+  let _id =
+    Classes.new_instance
+      ~program_mode ~global atts.polymorphic name bl t props pri in
+  ()
 
 let vernac_declare_instance ~atts id bl inst pri =
   let open DefAttributes in
@@ -2237,9 +2277,15 @@ let with_def_attributes ~atts f =
   if atts.DefAttributes.program then Obligations.check_program_libraries ();
   f ~atts
 
-let with_maybe_open_proof ~pstate f =
-  let opt = f ~pstate in
-  Proof_global.maybe_push ~ontop:pstate opt
+let with_read_proof ~pstate f =
+  f ~pstate;
+  pstate
+
+let with_open_proof ~pstate f =
+  Some (Proof_global.push ~ontop:pstate (f ~pstate))
+
+let with_open_proof_simple ~pstate f =
+  Some (Proof_global.push ~ontop:pstate f)
 
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2376,10 +2422,12 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.stack option =
     pstate
 
   (* Gallina *)
-  | VernacDefinition ((discharge,kind),lid,d) ->
-    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_definition discharge kind lid d)
+  | VernacDefinition (dk,lid,ProveBody(bl,t)) ->
+    with_open_proof ~pstate (with_def_attributes ~atts vernac_definition_interactive dk lid bl t)
+  | VernacDefinition (dk,lid,DefineBody(bl,red_option,c,typ_opt)) ->
+    with_read_proof ~pstate (with_def_attributes ~atts vernac_definition dk lid bl red_option c typ_opt)
   | VernacStartTheoremProof (k,l) ->
-    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_start_proof k l)
+    with_open_proof_simple ~pstate (with_def_attributes ~atts vernac_start_proof k l)
   | VernacEndProof e ->
     unsupported_attributes atts;
     vernac_end_proof ?proof ?pstate e
@@ -2393,9 +2441,17 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.stack option =
     vernac_inductive ~atts cum priv finite l;
     pstate
   | VernacFixpoint (discharge, l) ->
-    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_fixpoint discharge l)
+    let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in
+    if opens then
+      with_open_proof_simple ~pstate (with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
+    else
+      (with_def_attributes ~atts vernac_fixpoint discharge l; pstate)
   | VernacCoFixpoint (discharge, l) ->
-    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_cofixpoint discharge l)
+    let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in
+    if opens then
+      with_open_proof_simple ~pstate (with_def_attributes ~atts vernac_cofixpoint_interactive discharge l)
+    else
+      (with_def_attributes ~atts vernac_cofixpoint discharge l; pstate)
   | VernacScheme l ->
     unsupported_attributes atts;
     vernac_scheme l;
@@ -2465,8 +2521,20 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.stack option =
 
   (* Type classes *)
   | VernacInstance (name, bl, t, props, info) ->
-    with_maybe_open_proof ~pstate (fun ~pstate:_ ->
-        snd @@ with_def_attributes ~atts (vernac_instance name bl t props info))
+    if (DefAttributes.parse atts).DefAttributes.program then begin
+      with_def_attributes ~atts
+        (vernac_instance_program name bl t props info);
+      pstate
+    end else begin
+      match props with
+      | None ->
+        with_open_proof_simple ~pstate
+          (with_def_attributes ~atts
+            (vernac_instance_interactive name bl t info))
+      | Some props ->
+         with_def_attributes ~atts (vernac_instance name bl t props info);
+         pstate
+      end
   | VernacDeclareInstance (id, bl, inst, info) ->
     with_def_attributes ~atts vernac_declare_instance id bl inst info;
     pstate