summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_command.ml
blob: a83611a4f3a45af7c5065d8234f31b5492e66a49 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
open Closure
open RedFlags
open Declarations
open Entries
open Libobject
open Pattern
open Matching
open Pp
open Rawterm
open Sign
open Tacred
open Util
open Names
open Nameops
open Libnames
open Nametab
open Pfedit
open Proof_type
open Refiner
open Tacmach
open Tactic_debug
open Topconstr
open Term
open Termops
open Tacexpr
open Safe_typing
open Typing
open Hiddentac
open Genarg
open Decl_kinds
open Mod_subst
open Printer
open Inductiveops
open Syntax_def
open Environ
open Tactics
open Tacticals
open Tacinterp
open Vernacexpr
open Notation
open Evd
open Evarutil

module SPretyping = Subtac_pretyping.Pretyping
open Subtac_utils
open Pretyping
open Subtac_obligations

(*********************************************************************)
(* Functions to parse and interpret constructions *)

let evar_nf isevars c =
  Evarutil.nf_evar !isevars c

let interp_gen kind isevars env
               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
               c =
  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
  let c' = SPretyping.understand_tcc_evars isevars env kind c' in
    evar_nf isevars c'

let interp_constr isevars env c =
  interp_gen (OfType None) isevars env c

let interp_type_evars isevars env ?(impls=[]) c =
  interp_gen IsType isevars env ~impls c

let interp_casted_constr isevars env ?(impls=[]) c typ =
  interp_gen (OfType (Some typ)) isevars env ~impls c

let interp_casted_constr_evars isevars env ?(impls=[]) c typ =
  interp_gen (OfType (Some typ)) isevars env ~impls c

let interp_open_constr isevars env c =
    msgnl (str "Pretyping " ++ my_print_constr_expr c);
  let c = Constrintern.intern_constr ( !isevars) env c in
  let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in
    evar_nf isevars c'

let interp_constr_judgment isevars env c =
  let j =
    SPretyping.understand_judgment_tcc isevars env
      (Constrintern.intern_constr ( !isevars) env c)
  in
    { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }

let locate_if_isevar loc na = function
  | RHole _ ->
      (try match na with
	| Name id ->  Reserve.find_reserved_type id
	| Anonymous -> raise Not_found
      with Not_found -> RHole (loc, Evd.BinderType na))
  | x -> x

let interp_binder sigma env na t =
  let t = Constrintern.intern_gen true ( !sigma) env t in
    SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)

let interp_context_evars evdref env params =
  let bl = Constrintern.intern_context false ( !evdref) env params in
  let (env, par, _, impls) =
    List.fold_left
      (fun (env,params,n,impls) (na, k, b, t) ->
	match b with
	    None ->
	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
	      let t = SPretyping.understand_tcc_evars evdref env IsType t' in
	      let d = (na,None,t) in
	      let impls =
		if k = Implicit then
		  let na = match na with Name n -> Some n | Anonymous -> None in
		    (ExplByPos (n, na), (true, true, true)) :: impls
		else impls
	      in
		(push_rel d env, d::params, succ n, impls)
	  | Some b ->
	      let c = SPretyping.understand_judgment_tcc evdref env b in
	      let d = (na, Some c.uj_val, c.uj_type) in
		(push_rel d env,d::params, succ n, impls))
      (env,[],1,[]) (List.rev bl)
  in (env, par), impls

(* try to find non recursive definitions *)

let list_chop_hd i l = match list_chop i l with
  | (l1,x::l2) -> (l1,x,l2)
  | (x :: [], l2) -> ([], x, [])
  | _ -> assert(false)

let collect_non_rec env =
  let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
    try
      let i =
        list_try_find_i
          (fun i f ->
             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
             then i else failwith "try_find_i")
          0 lnamerec
      in
      let (lf1,f,lf2) = list_chop_hd i lnamerec in
      let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
      let (lar1,ar,lar2) = list_chop_hd i larrec in
      let newlnv =
	try
	  match list_chop i nrec with
            | (lnv1,_::lnv2) -> (lnv1@lnv2)
	    | _ -> [] (* nrec=[] for cofixpoints *)
        with Failure "list_chop" -> []
      in
      searchrec ((f,def,ar)::lnonrec)
	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
    with Failure "try_find_i" ->
      (List.rev lnonrec,
       (Array.of_list lnamerec, Array.of_list ldefrec,
        Array.of_list larrec, Array.of_list nrec))
  in
  searchrec []

let list_of_local_binders l =
  let rec aux acc = function
      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
    | Topconstr.LocalRawAssum (nl, k, c) :: tl ->
	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
    | [] -> List.rev acc
  in aux [] l

let lift_binders k n l =
  let rec aux n = function
    | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
    | [] -> []
  in aux n l

let rec gen_rels = function
    0 -> []
  | n -> mkRel n :: gen_rels (pred n)

let split_args n rel = match list_chop ((List.length rel) - n) rel with
    (l1, x :: l2) -> l1, x, l2
  | _ -> assert(false)

open Coqlib

let sigT = Lazy.lazy_from_fun build_sigma_type
let sigT_info = lazy
  { ci_ind       = destInd (Lazy.force sigT).typ;
    ci_npar      = 2;
    ci_cstr_nargs = [|2|];
    ci_pp_info   =  { ind_nargs = 0; style = LetStyle }
  }

let telescope = function
  | [] -> assert false
  | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
  | (n, None, t) :: tl ->
      let ty, tys, (k, constr) =
	List.fold_left
	  (fun (ty, tys, (k, constr)) (n, b, t) ->
	    let pred = mkLambda (n, t, ty) in
	    let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
	    let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
	      (sigty, pred :: tys, (succ k, intro)))
	  (t, [], (2, mkRel 1)) tl
      in
      let (last, subst) = List.fold_right2
	(fun pred (n, b, t) (prev, subst) ->
	  let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in
	  let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in
	    (lift 1 proj2, (n, Some proj1, t) :: subst))
	(List.rev tys) tl (mkRel 1, [])
      in ty, ((n, Some last, t) :: subst), constr

  | _ -> raise (Invalid_argument "telescope")

let nf_evar_context isevars ctx =
  List.map (fun (n, b, t) ->
    (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx

let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
  Coqlib.check_required_library ["Coq";"Program";"Wf"];
  let sigma = Evd.empty in
  let isevars = ref (Evd.create_evar_defs sigma) in
  let env = Global.env() in
  let _pr c = my_print_constr env c in
  let _prr = Printer.pr_rel_context env in
  let _prn = Printer.pr_named_context env in
  let _pr_rel env = Printer.pr_rel_context env in
  let (env', binders_rel), impls = interp_context_evars isevars env bl in
  let len = List.length binders_rel in
  let top_env = push_rel_context binders_rel env in
  let top_arity = interp_type_evars isevars top_env arityc in
  let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
  let argtyp, letbinders, make = telescope binders_rel in
  let argname = id_of_string "recarg" in
  let arg = (Name argname, None, argtyp) in
  let binders = letbinders @ [arg] in
  let binders_env = push_rel_context binders_rel env in
  let rel = interp_constr isevars env r in
  let relty = type_of env !isevars rel in
  let relargty =
    let error () =
      user_err_loc (constr_loc r,
		   "Subtac_command.build_wellfounded",
		   my_print_constr env rel ++ str " is not an homogeneous binary relation.")
    in
      try
	let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
	  match ctx, kind_of_term ar with
	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
	      when Reductionops.is_conv env !isevars t u -> t
	  | _, _ -> error ()
      with _ -> error ()
  in
  let measure = interp_casted_constr isevars binders_env measure relargty in
  let wf_rel, wf_rel_fun, measure_fn =
    let measure_body, measure =
      it_mkLambda_or_LetIn measure letbinders,
      it_mkLambda_or_LetIn measure binders
    in
    let comb = constr_of_global (delayed_force measure_on_R_ref) in
    let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
    let wf_rel_fun x y =
      mkApp (rel, [| subst1 x measure_body;
 		     subst1 y measure_body |])
    in wf_rel, wf_rel_fun, measure
  in
  let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
  let argid' = id_of_string (string_of_id argname ^ "'") in
  let wfarg len = (Name argid', None,
  		  mkSubset (Name argid') argtyp
		    (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
  in
  let intern_bl = wfarg 1 :: [arg] in
  let _intern_env = push_rel_context intern_bl env in
  let proj = (delayed_force sig_).Coqlib.proj1 in
  let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
  let projection = (* in wfarg :: arg :: before *)
    mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
  in
  let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in
  let intern_arity = substl [projection] top_arity_let in
  (* substitute the projection of wfarg for something,
     now intern_arity is in wfarg :: arg *)
  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
  let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
  let curry_fun =
    let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
    let arg = mkApp ((delayed_force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
    let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
    let rcurry = mkApp (rel, [| measure; lift len measure |]) in
    let lam = (Name (id_of_string "recproof"), None, rcurry) in
    let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
    let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
      (Name recname, Some body, ty)
  in
  let fun_bl = intern_fun_binder :: [arg] in
  let lift_lets = Termops.lift_rel_context 1 letbinders in
  let intern_body =
    let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
    let (r, l, impls, scopes) =
      Constrintern.compute_internalization_data env
	Constrintern.Recursive full_arity impls 
    in
    let newimpls = [(recname, (r, l, impls @ 
      [Some (id_of_string "recproof", Impargs.Manual, (true, false))], 
			      scopes @ [None]))] in
    interp_casted_constr isevars ~impls:newimpls
      (push_rel_context ctx env) body (lift 1 top_arity)
  in
  let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
  let prop = mkLambda (Name argname, argtyp, top_arity_let) in
  let def =
    mkApp (constr_of_global (delayed_force fix_sub_ref),
	  [| argtyp ; wf_rel ;
	     make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
	     prop ; intern_body_lam |])
  in
  let _ = isevars := Evarutil.nf_evar_map !isevars in
  let binders_rel = nf_evar_context !isevars binders_rel in
  let binders = nf_evar_context !isevars binders in
  let top_arity = Evarutil.nf_evar !isevars top_arity in
  let hook, recname, typ = 
    if List.length binders_rel > 1 then
      let name = add_suffix recname "_func" in
      let hook l gr = 
	let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
	let ty = it_mkProd_or_LetIn top_arity binders_rel in
	let ce =
	  { const_entry_body = Evarutil.nf_evar !isevars body;
	    const_entry_type = Some ty;
	    const_entry_opaque = false;
	    const_entry_boxed = false} 
	in 
	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
	let gr = ConstRef c in
	  if Impargs.is_implicit_args () || impls <> [] then
	    Impargs.declare_manual_implicits false gr [impls]
      in
      let typ = it_mkProd_or_LetIn top_arity binders in
	hook, name, typ
    else 
      let typ = it_mkProd_or_LetIn top_arity binders_rel in
      let hook l gr = 
	if Impargs.is_implicit_args () || impls <> [] then
	  Impargs.declare_manual_implicits false gr [impls]
      in hook, recname, typ
  in
  let fullcoqc = Evarutil.nf_evar !isevars def in
  let fullctyp = Evarutil.nf_evar !isevars typ in
  let evm = evars_of_term !isevars Evd.empty fullctyp in
  let evm = evars_of_term !isevars evm fullcoqc in
  let evm = non_instanciated_map env isevars evm in
  let evars, _, evars_def, evars_typ = 
    Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp 
  in
    Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook

let interp_fix_context evdref env fix =
  interp_context_evars evdref env fix.Command.fix_binders

let interp_fix_ccl evdref (env,_) fix =
  interp_type_evars evdref env fix.Command.fix_type

let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
  let env = push_rel_context ctx env_rec in
  let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in
  Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body

let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx

let prepare_recursive_declaration fixnames fixtypes fixdefs =
  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
  let names = List.map (fun id -> Name id) fixnames in
  (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)

let rel_index n ctx =
  list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))

let rec unfold f b =
  match f b with
    | Some (x, b') -> x :: unfold f b'
    | None -> []

let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
  match n with
  | Some (loc, n) -> [rel_index n fixctx]
  | None ->
      (* If recursive argument was not given by user, we try all args.
	 An earlier approach was to look only for inductive arguments,
	 but doing it properly involves delta-reduction, and it finally
         doesn't seem to worth the effort (except for huge mutual
	 fixpoints ?) *)
      let len = List.length fixctx in
	unfold (function x when x = len -> None
	  | n -> Some (n, succ n)) 0

let push_named_context = List.fold_right push_named

let check_evars env initial_sigma evd c =
  let sigma =  evd in
  let c = nf_evar sigma c in
  let rec proc_rec c =
    match kind_of_term c with
      | Evar (evk,args) ->
          assert (Evd.mem sigma evk);
	  if not (Evd.mem initial_sigma evk) then
            let (loc,k) = evar_source evk evd in
	      (match k with
	      | QuestionMark _
	      | ImplicitArg (_, _, false) -> ()
	      | _ ->
		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
      | _ -> iter_constr proc_rec c
  in proc_rec c

let out_def = function
  | Some def -> def
  | None -> error "Program Fixpoint needs defined bodies."

let interp_recursive fixkind l boxed =
  let env = Global.env() in
  let fixl, ntnl = List.split l in
  let kind = fixkind <> IsCoFixpoint in
  let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in

  (* Interp arities allowing for unresolved types *)
  let evdref = ref Evd.empty in
  let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
  let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
  let fixtypes = List.map2 build_fix_type fixctxs fixccls in
  let rec_sign =
    List.fold_left2 (fun env' id t ->
      let sort = Retyping.get_type_of env !evdref t in
      let fixprot =
	try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
	with e -> t
      in
	(id,None,fixprot) :: env')
      [] fixnames fixtypes
  in
  let env_rec = push_named_context rec_sign env in

  (* Get interpretation metadatas *)
  let impls = Constrintern.compute_internalization_env env
    Constrintern.Recursive fixnames fixtypes fiximps
  in
  let notations = List.flatten ntnl in

  (* Interp bodies with rollback because temp use of notations/implicit *)
  let fixdefs =
    States.with_state_protection (fun () ->
      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
      list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
      () in

  let fixdefs = List.map out_def fixdefs in

  (* Instantiate evars and check all are resolved *)
  let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in
  let evd = Typeclasses.resolve_typeclasses
    ~onlyargs:true ~split:true ~fail:false env_rec evd
  in
  let evd = Evarutil.nf_evar_map evd in
  let fixdefs = List.map (nf_evar evd) fixdefs in
  let fixtypes = List.map (nf_evar evd) fixtypes in
  let rec_sign = nf_named_context_evar evd rec_sign in

  let recdefs = List.length rec_sign in
  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
  List.iter (check_evars env Evd.empty evd) fixtypes;
  Command.check_mutuality env kind (List.combine fixnames fixdefs);

  (* Russell-specific code *)

  (* Get the interesting evars, those that were not instanciated *)
  let isevars = Evd.undefined_evars evd in
  let evm =  isevars in
  (* Solve remaining evars *)
  let rec collect_evars id def typ imps =
      (* Generalize by the recursive prototypes  *)
    let def =
      Termops.it_mkNamedLambda_or_LetIn def rec_sign
    and typ =
      Termops.it_mkNamedProd_or_LetIn typ rec_sign
    in
    let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
    let evm' = Subtac_utils.evars_of_term evm evm' typ in
    let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
      (id, def, typ, imps, evars)
  in
  let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
    (match fixkind with
      | IsFixpoint wfl ->
	  let possible_indexes =
	    list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
	    Array.of_list fixtypes,
	    Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
	  in
	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
	    list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
      | IsCoFixpoint -> ());
    Subtac_obligations.add_mutual_definitions defs notations fixkind

let out_n = function
    Some n -> n
  | None -> raise Not_found

let build_recursive l b =
  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
    match g, l with
	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
	  ignore(build_wellfounded (id, n, bl, typ, out_def def) r
		    (match n with Some n -> mkIdentC (snd n) | None ->
		      errorlabstrm "Subtac_command.build_recursive"
			(str "Recursive argument required for well-founded fixpoints"))
		    ntn false)

      | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
	  ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
		    m ntn false)

      | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
	  let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
	      Command.fix_body = def; Command.fix_type = typ},ntn)) l
	  in interp_recursive (IsFixpoint g) fixl b
      | _, _ ->
	  errorlabstrm "Subtac_command.build_recursive"
	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")

let build_corecursive l b =
  let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
      Command.fix_body = def; Command.fix_type = typ},ntn))
    l in
  interp_recursive IsCoFixpoint fixl b