From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- contrib/subtac/subtac_command.ml | 389 ++++++++++++++++++++------------------- 1 file changed, 203 insertions(+), 186 deletions(-) (limited to 'contrib/subtac/subtac_command.ml') diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 86139039..5bff6ad1 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -39,6 +39,8 @@ open Tacticals open Tacinterp open Vernacexpr open Notation +open Evd +open Evarutil module SPretyping = Subtac_pretyping.Pretyping open Subtac_utils @@ -53,22 +55,24 @@ let evar_nf isevars c = Evarutil.nf_isevar !isevars c let interp_gen kind isevars env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in -(* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) + let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in let c' = SPretyping.pretype_gen 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 isevars env ?(impls=([],[])) 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 (Evd.evars_of !isevars) env c in @@ -92,26 +96,31 @@ let locate_if_isevar loc na = function let interp_binder sigma env na t = let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in - SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t) - - -let interp_context sigma env params = - List.fold_left - (fun (env,params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> - let t = interp_binder sigma env na t in - let d = (na,None,t) in - (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> - let t = interp_type sigma env t in - let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in - let ctx = List.rev ctx in - (push_rel_context ctx env, ctx@params) - | LocalRawDef ((_,na),c) -> - let c = interp_constr_judgment sigma env c in - let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env,d::params)) - (env,[]) params + SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t) + +let interp_context_evars evdref env params = + let bl = Constrintern.intern_context (Evd.evars_of !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)) :: 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 *) @@ -126,7 +135,7 @@ let collect_non_rec env = let i = list_try_find_i (fun i f -> - if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec + if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec then i else failwith "try_find_i") 0 lnamerec in @@ -152,14 +161,14 @@ let collect_non_rec env = 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, c) :: 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 + | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl | [] -> [] in aux n l @@ -172,11 +181,10 @@ let split_args n rel = match list_chop ((List.length rel) - n) rel with | _ -> assert(false) 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 nc = named_context env in - let nc_len = named_context_length nc 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 @@ -188,8 +196,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* Ppconstr.pr_constr_expr body) *) (* with _ -> () *) (* in *) - let env', binders_rel = interp_context isevars env bl in - let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in + let (env', binders_rel), impls = interp_context_evars isevars env bl in + let after, ((argname, _, argtyp) as arg), before = + let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in + split_args idx binders_rel in let before_length, after_length = List.length before, List.length after in let argid = match argname with Name n -> n | _ -> assert(false) in let liftafter = lift_binders 1 after_length after in @@ -226,11 +236,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1)))) in let top_bl = after @ (arg :: before) in - let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in - (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ()); let top_env = push_rel_context top_bl env in + let top_arity = interp_type_evars isevars top_env arityc in + let intern_bl = wfarg 1 :: arg :: before in let _intern_env = push_rel_context intern_bl env in - let top_arity = interp_type isevars top_env arityc in let proj = (Lazy.force sig_).Coqlib.proj1 in let projection = mkApp (proj, [| argtyp ; @@ -240,29 +249,21 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = |]) in let intern_arity = it_mkProd_or_LetIn top_arity after in - (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity); - trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ()); - (* Top arity is in top_env = after :: arg :: before *) -(* let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *) -(* (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *) -(* trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *) - let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *) - (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); -(* let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *) -(* (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *) + (* Intern arity is in top_env = arg :: before *) + let intern_arity = liftn 2 2 intern_arity in +(* trace (str "After lifting arity: " ++ *) +(* my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *) +(* intern_arity); *) + (* arity is now in something :: wfarg :: arg :: before + where what refered to arg now refers to something *) + let intern_arity = substl [projection] intern_arity in + (* substitute the projection of wfarg for something *) let intern_before_env = push_rel_context before env in -(* let intern_fun_bl = liftafter @ [wfarg 1] in (\* FixMe dependencies *\) *) -(* (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *) - (try trace (str "Intern arity: " ++ - my_print_constr _intern_env intern_arity) with _ -> ()); let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in - (try trace (str "Intern fun arity product: " ++ - my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ()); let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in -(* (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *) let fun_env = push_rel_context fun_bl intern_before_env in - let fun_arity = interp_type isevars fun_env arityc in + let fun_arity = interp_type_evars isevars fun_env arityc in let intern_body = interp_casted_constr isevars fun_env body fun_arity in let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in let _ = @@ -274,161 +275,177 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* str "Intern body " ++ pr intern_body_lam) *) with _ -> () in - let _impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits top_env top_arity - else [] - in let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in + (* Lift to get to constant arguments *) + let lift_cst = List.length after + 1 in let fix_def = match measure_fn with None -> - mkApp (constr_of_reference (Lazy.force fix_sub_ref), + mkApp (constr_of_global (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ; - prop ; - intern_body_lam |]) + make_existential dummy_loc ~opaque:false env isevars wf_proof ; + lift lift_cst prop ; + lift lift_cst intern_body_lam |]) | Some f -> - lift (succ after_length) - (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), - [| argtyp ; - f ; - prop ; - intern_body_lam |])) + mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), + [| lift lift_cst argtyp ; + lift lift_cst f ; + lift lift_cst prop ; + lift lift_cst intern_body_lam |]) in let def_appl = applist (fix_def, gen_rels (after_length + 1)) in let def = it_mkLambda_or_LetIn def_appl binders_rel in let typ = it_mkProd_or_LetIn top_arity binders_rel in let fullcoqc = Evarutil.nf_isevar !isevars def in let fullctyp = Evarutil.nf_isevar !isevars typ in -(* let _ = try trace (str "After evar normalization: " ++ spc () ++ *) -(* str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *) -(* ++ str "Coq type: " ++ my_print_constr env fullctyp) *) -(* with _ -> () *) -(* in *) let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in let evm = non_instanciated_map env isevars evm in - - (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in - (* (try trace (str "Generated obligations : "); *) -(* Array.iter *) - (* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *) - (* evars; *) - (* with _ -> ()); *) - Subtac_obligations.add_definition recname evars_def fullctyp evars + let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in + Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> - (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx + (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx -let build_mutrec l boxed = - let sigma = Evd.empty and env = Global.env () in - let nc = named_context env in - let nc_len = named_context_length nc in - let lnameargsardef = - (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env protos (f, d))*) - l - in - let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef - and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef +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 = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in + it_mkLambda_or_LetIn body ctx + +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 interp_recursive fixkind l boxed = + let env = Global.env() in + let fixl, ntnl = List.split l in + let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in + + (* Interp arities allowing for unresolved types *) + let evdref = ref (Evd.create_evar_defs 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 -> (id,None,t) :: env) + [] fixnames fixtypes in - (* Build the recursive context and notations for the recursive types *) - let (rec_sign,rec_env,rec_impls,arityl) = - List.fold_left - (fun (sign,env,impls,arl) ((recname, n, bl,arityc,body),_) -> - let isevars = ref (Evd.create_evar_defs sigma) in - let arityc = Command.generalize_constr_expr arityc bl in - let arity = interp_type isevars env arityc in - let impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits env arity - else [] in - let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in - ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)) - ([],env,[],[]) lnameargsardef in - let arityl = List.rev arityl in - let notations = - List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) - lnameargsardef [] in - - let recdef = - - (* Declare local notations *) - let fs = States.freeze() in + let env_rec = push_named_context rec_sign env in + + (* Get interpretation metadatas *) + let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in + let notations = List.fold_right Option.List.cons ntnl [] in + + (* Interp bodies with rollback because temp use of notations/implicit *) + let fixdefs = + States.with_heavy_rollback (fun () -> + List.iter (Command.declare_interning_data impls) notations; + list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) + () in + + (* Instantiate evars and check all are resolved *) + let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in + let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in + let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in + let rec_sign = nf_named_context_evar (evars_of 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; *) +(* 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 + trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars); + let evm = Evd.evars_of isevars in + trace (str "got the evm, recdefs is " ++ int recdefs); + (* Solve remaining evars *) + let rec collect_evars id def typ imps = + let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in + (* Generalize by the recursive prototypes *) let def = - try - List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) - Metasyntax.add_notation_interpretation df rec_impls c None) notations; - List.map2 - (fun ((_,_,bl,_,def),_) (isevars, info, arity) -> - match info with - None -> - let def = abstract_constr_expr def bl in - isevars, info, interp_casted_constr isevars rec_env ~impls:([],rec_impls) - def arity - | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) -> - let rec_env = push_rel_context fun_bl rec_env in - let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls) - def intern_arity - in isevars, info, it_mkLambda_or_LetIn cstr fun_bl) - lnameargsardef arityl - with e -> - States.unfreeze fs; raise e in - States.unfreeze fs; def - in - let (lnonrec,(namerec,defrec,arrec,nvrec)) = - collect_non_rec env lrecnames recdef arityl nv in - let recdefs = Array.length defrec in - (* Solve remaining evars *) - let rec collect_evars i acc = - if i < recdefs then - let (isevars, info, def) = defrec.(i) in - (* let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *) - let def = evar_nf isevars def in - let x, y, typ = arrec.(i) in - let typ = evar_nf isevars typ in - arrec.(i) <- (x, y, typ); - let rec_sign = nf_evar_context !isevars rec_sign in - let isevars = Evd.undefined_evars !isevars in - (* let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *) - let evm = Evd.evars_of isevars in - let id = namerec.(i) in - (* 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 evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in - collect_evars (succ i) ((id, def, typ, evars) :: acc) - else acc + 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 = collect_evars 0 [] in - Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec - + let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in + (match fixkind with + | Command.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 + | Command.IsCoFixpoint -> ()); + Subtac_obligations.add_mutual_definitions defs notations fixkind + let out_n = function Some n -> n - | None -> 0 - -let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed = - match lnameargsardef with - | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> - build_wellfounded (id, out_n n, bl, typ, body) r false no boxed - | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> - build_wellfounded (id, out_n n, bl, typ, body) r true no boxed - | l -> - let lnameargsardef = - List.map (fun ((id, (n, ro), bl, typ, body), no) -> - match ro with - CStructRec -> (id, out_n n, bl, typ, body), no - | CWfRec _ | CMeasureRec _ -> - errorlabstrm "Subtac_command.build_recursive" - (str "Well-founded fixpoints not allowed in mutually recursive blocks")) - lnameargsardef - in build_mutrec lnameargsardef boxed - - - + | 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, out_n n, bl, typ, def) r false ntn false) + + | [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] -> + ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false) + + | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> + let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> + ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l + in interp_recursive (Command.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_body = def; Command.fix_type = typ},ntn)) + l in + interp_recursive Command.IsCoFixpoint fixl b -- cgit v1.2.3