- { status with proof_status = Incomplete_proof (initial_proof,goalno)}
- | _ ->
- if metasenv <> [] then
- command_error (
- "metasenv not empty while giving a definition with body: " ^
- CicMetaSubst.ppmetasenv metasenv []);
- let status = MatitaSync.add_obj uri obj status in
- match obj with
- Cic.Constant _ -> status
- | Cic.InductiveDefinition (_,_,_,attrs) ->
- let status = generate_elimination_principles uri status in
- let rec get_record_attrs =
- function
- [] -> None
- | (`Class (`Record fields))::_ -> Some fields
- | _::tl -> get_record_attrs tl
- in
- (match get_record_attrs attrs with
- None -> status (* not a record *)
- | Some fields -> generate_projections uri fields status)
- | Cic.CurrentProof _
- | Cic.Variable _ -> assert false
+ { status with proof_status = Incomplete_proof (initial_proof,goalno)}
+ | _ ->
+ if metasenv <> [] then
+ command_error (
+ "metasenv not empty while giving a definition with body: " ^
+ CicMetaSubst.ppmetasenv metasenv []);
+ let status = MatitaSync.add_obj uri obj status in
+ match obj with
+ Cic.Constant _ -> status
+ | Cic.InductiveDefinition (_,_,_,attrs) ->
+ let status = generate_elimination_principles uri status in
+ let rec get_record_attrs =
+ function
+ [] -> None
+ | (`Class (`Record fields))::_ -> Some fields
+ | _::tl -> get_record_attrs tl
+ in
+ (match get_record_attrs attrs with
+ None -> status (* not a record *)
+ | Some fields -> generate_projections uri fields status)
+ | Cic.CurrentProof _
+ | Cic.Variable _ -> assert false