diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 437 |
1 files changed, 96 insertions, 341 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 8ed99cbd..511befd8 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 11161 2008-06-21 14:32:47Z msozeau $ i*) +(*i $Id: classes.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Names @@ -50,22 +50,23 @@ let declare_instance_cst glob con = let _, r = decompose_prod_assum instance in match class_of_constr r with | Some tc -> add_instance (new_instance tc None glob con) - | None -> error "Constant does not build instances of a declared type class" + | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") let declare_instance glob idl = let con = try (match global (Ident idl) with | ConstRef x -> x | _ -> raise Not_found) - with _ -> error "Instance definition not found" + with _ -> error "Instance definition not found." in declare_instance_cst glob con let mismatched_params env n m = mismatched_ctx_inst env Parameters n m -(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *) let mismatched_props env n m = mismatched_ctx_inst env Properties n m type binder_list = (identifier located * bool * constr_expr) list +(* Calls to interpretation functions. *) + let interp_binders_evars isevars env avoid l = List.fold_left (fun (env, ids, params) ((loc, i), t) -> @@ -87,111 +88,6 @@ let interp_typeclass_context_evars isevars env avoid l = (push_named d env, i :: ids, d::params)) (env, avoid, []) l -let interp_constrs_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) t -> - let t' = interp_binder_evars isevars env Anonymous t in - let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in - let d = (id,None,t') in - (push_named d env, id :: ids, d::params)) - (env, avoid, []) l - -let raw_assum_of_binders k = - List.map (fun ((loc,i),t) -> LocalRawAssum ([(loc, Name i)], k, t)) - -let raw_assum_of_constrs k = - List.map2 (fun t (n,_,_) -> LocalRawAssum ([(dummy_loc, Name n)], k, t)) - -let raw_assum_of_anonymous_constrs k = - List.map (fun t -> LocalRawAssum ([(dummy_loc, Anonymous)], k, t)) - -let decl_expr_of_binders = - List.map (fun ((loc,i),t) -> false, Vernacexpr.AssumExpr ((loc, Name i), t)) - -let rec unfold n f acc = - match n with - | 0 -> f 0 acc - | n -> unfold (n - 1) f (f n acc) - -(* Declare everything in the parameters as implicit, and the class instance as well *) -open Topconstr - -let declare_implicit_proj c proj imps sub = - let len = List.length c.cl_context in - let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) (snd proj)) in - let expls = - let rec aux i expls = function - [] -> expls - | (Name n, _) :: tl -> - let impl = ExplByPos (i, Some n), (true, true) in - aux (succ i) (impl :: List.remove_assoc (ExplByName n) expls) tl - | (Anonymous,_) :: _ -> assert(false) - in - aux 1 [] (List.rev ctx) - in - let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in - if sub then - declare_instance_cst true (snd proj); - Impargs.declare_manual_implicits false (ConstRef (snd proj)) true expls - -let declare_implicits impls subs cl = - Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub) - cl.cl_projs impls subs; - let len = List.length cl.cl_context in - let indimps = - list_fold_left_i - (fun i acc (is, (na, b, t)) -> - if len - i <= cl.cl_params then acc - else - match is with - None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc - | _ -> acc) - 1 [] (List.rev cl.cl_context) - in - Impargs.declare_manual_implicits false cl.cl_impl false indimps - -let rel_of_named_context subst l = - List.fold_right - (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc) - l ([], subst) - -let ids_of_rel_context subst l = - List.fold_right - (fun (id, _, t) acc -> Nameops.out_name id :: acc) - l subst - -let degenerate_decl (na,b,t) = - let id = match na with - | Name id -> id - | Anonymous -> anomaly "Unnamed record variable" in - match b with - | None -> (id, Entries.LocalAssum t) - | Some b -> (id, Entries.LocalDef b) - - -let declare_structure env id idbuild params arity fields = - let nparams = List.length params and nfields = List.length fields in - let args = extended_rel_list nfields params in - let ind = applist (mkRel (1+nparams+nfields), args) in - let type_constructor = it_mkProd_or_LetIn ind fields in - let mie_ind = - { mind_entry_typename = id; - mind_entry_arity = arity; - mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } in - let mie = - { mind_entry_params = List.map degenerate_decl params; - mind_entry_record = true; - mind_entry_finite = true; - mind_entry_inds = [mie_ind] } in - let kn = Command.declare_mutual_with_eliminations true mie [] in - let rsp = (kn,0) in (* This is ind path of idstruc *) - let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in - let kinds,sp_projs = Record.declare_projections rsp ~kind:Method ~name:id (List.map (fun _ -> false) fields) fields in - let _build = ConstructRef (rsp,1) in - Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs); - rsp - let interp_type_evars evdref env ?(impls=([],[])) typ = let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in @@ -206,19 +102,31 @@ let interp_fields_evars isevars env avoid l = (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> let impl, t' = interp_type_evars isevars env ~impls t in let data = mk_interning_data env i impl t' in - let d = (i,None,t') in - (push_named d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls))) - (env, [], avoid, [], ([], [])) l - -let interp_fields_rel_evars isevars env avoid l = - List.fold_left - (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> - let impl, t' = interp_type_evars isevars env ~impls t in - let data = mk_interning_data env i impl t' in let d = (Name i,None,t') in (push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls))) (env, [], avoid, [], ([], [])) l +(* Declare everything in the parameters as implicit, and the class instance as well *) + +open Topconstr + +let implicits_of_context ctx = + list_map_i (fun i name -> + let explname = + match name with + | Name n -> Some n + | Anonymous -> None + in ExplByPos (i, explname), (true, true)) + 1 (List.rev (Anonymous :: (List.map pi1 ctx))) + +let degenerate_decl (na,b,t) = + let id = match na with + | Name id -> id + | Anonymous -> anomaly "Unnamed record variable" in + match b with + | None -> (id, Entries.LocalAssum t) + | Some b -> (id, Entries.LocalDef b) + let name_typeclass_binder avoid = function | LocalRawAssum ([loc, Anonymous], bk, c) -> let name = @@ -237,33 +145,7 @@ let name_typeclass_binders avoid l = b' :: binders, avoid) ([], avoid) l in List.rev l', avoid - -let decompose_named_assum = - let rec prodec_rec subst l c = - match kind_of_term c with - | Prod (Name na,t,c) -> - let decl = (na,None,substl subst t) in - let subst' = mkVar na :: subst in - prodec_rec subst' (add_named_decl decl l) (substl subst' c) - | LetIn (Name na, b, t, c) -> - let decl = (na,Some (substl subst b),substl subst t) in - let subst' = mkVar na :: subst in - prodec_rec subst' (add_named_decl decl l) (substl subst' c) - | Cast (c,_,_) -> prodec_rec subst l c - | _ -> l,c - in prodec_rec [] [] -let push_named_context = - List.fold_right push_named - -let named_of_rel_context (subst, ids, env as init) ctx = - Sign.fold_rel_context - (fun (na,c,t) (subst, avoid, env) -> - let id = Nameops.next_name_away na avoid in - let d = (id,Option.map (substl subst) c,substl subst t) in - (mkVar id :: subst, id::avoid, d::env)) - ctx ~init - let new_class id par ar sup props = let env0 = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in @@ -294,7 +176,7 @@ let new_class id par ar sup props = (* Interpret the definitions and propositions *) let env_props, prop_impls, bound, ctx_props, _ = - interp_fields_rel_evars isevars env_params bound props + interp_fields_evars isevars env_params bound props in let subs = List.map (fun ((loc, id), b, _) -> b) props in (* Instantiate evars and check all are resolved *) @@ -305,6 +187,12 @@ let new_class id par ar sup props = let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in let arity = Reductionops.nf_evar sigma arity in let ce t = Evarutil.check_evars env0 Evd.empty isevars t in + let fieldimpls = + (* Make the class and all params implicits in the projections *) + let ctx_impls = implicits_of_context ctx_params in + let len = succ (List.length ctx_params) in + List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls + in let impl, projs = let params = ctx_params and fields = ctx_props in List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); @@ -337,31 +225,34 @@ let new_class id par ar sup props = let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) in - ConstRef cst, [proj_name, proj_cst] + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps; + Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls); + cref, [proj_name, proj_cst] | _ -> let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in - let kn = declare_structure env0 (snd id) idb params arity fields in - IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) - fields (Recordops.lookup_projections kn)) + let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in + let kn = Record.declare_structure (snd id) idb arity_imps + params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) + in + IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) + fields (Recordops.lookup_projections (kn,0))) in - let ids = List.map pi1 (named_context env0) in - let (subst, ids, named_ctx_params) = named_of_rel_context ([], ids, []) ctx_params in - let (_, _, named_ctx_props) = named_of_rel_context (subst, ids, []) ctx_props in let ctx_context = List.map (fun ((na, b, t) as d) -> match Typeclasses.class_of_constr t with - | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = Name na) supnames), d) + | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d) | None -> (None, d)) - named_ctx_params + ctx_params in let k = { cl_impl = impl; - cl_params = List.length par; cl_context = ctx_context; - cl_props = named_ctx_props; + cl_props = ctx_props; cl_projs = projs } in - declare_implicits (List.rev prop_impls) subs k; + List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p)) + k.cl_projs subs; add_class k type binder_def_list = (identifier located * identifier located list * constr_expr) list @@ -369,63 +260,16 @@ type binder_def_list = (identifier located * identifier located list * constr_ex let binders_of_lidents l = List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l -let subst_ids_in_named_context subst l = - let x, _ = - List.fold_right - (fun (id, _, t) (ctx, k) -> (id, None, substn_vars k subst t) :: ctx, succ k) - l ([], 1) - in x - -let subst_one_named inst ids t = - substnl inst 0 (substn_vars 1 ids t) - -let subst_named inst subst ctx = - let ids = List.map (fun (id, _, _) -> id) subst in - let ctx' = subst_ids_in_named_context ids ctx in - let ctx', _ = - List.fold_right - (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k) - ctx' ([], 0) - in ctx' -(* -let infer_super_instances env params params_ctx super = - let super = subst_named params params_ctx super in - List.fold_right - (fun (na, _, t) (sups, ids, supctx) -> - let t = subst_one_named sups ids t in - let inst = - try resolve_one_typeclass env t - with Not_found -> - let cl, args = destClass t in - no_instance (push_named_context supctx env) (dummy_loc, cl.cl_name) (Array.to_list args) - in - let d = (na, Some inst, t) in - inst :: sups, na :: ids, d :: supctx) - super ([], [], [])*) - -(* let evars_of_context ctx id n env = *) -(* List.fold_right (fun (na, _, t) (n, env, nc) -> *) -(* let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (Ident id, (n * Some na))) t in *) -(* let d = (na, Some b, t) in *) -(* (succ n, push_named d env, d :: nc)) *) -(* ctx (n, env, []) *) - let type_ctx_instance isevars env ctx inst subst = - List.fold_left2 - (fun (subst, instctx) (na, _, t) ce -> - let t' = replace_vars subst t in - let c = interp_casted_constr_evars isevars env ce t' in - let d = na, Some c, t' in - (na, c) :: subst, d :: instctx) - (subst, []) (List.rev ctx) inst - -let substitution_of_constrs ctx cstrs = - List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] - -let destClassApp cl = - match cl with - | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l - | _ -> raise Not_found + let (s, _) = + List.fold_left2 + (fun (subst, instctx) (na, _, t) ce -> + let t' = substl subst t in + let c = interp_casted_constr_evars isevars env ce t' in + let d = na, Some c, t' in + c :: subst, d :: instctx) + (subst, []) (List.rev ctx) inst + in s let refine_ref = ref (fun _ -> assert(false)) @@ -521,31 +365,31 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let imps, c' = interp_type_evars isevars env c in - let ctx, c = decompose_named_assum c' in + let ctx, c = decompose_prod_assum c' in let cl, args = Typeclasses.dest_class_app c in - cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) + cl, ctx, imps, List.rev (Array.to_list args) in let id = match snd instid with Name id -> let sp = Lib.make_path id in if Nametab.exists_cci sp then - errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); + errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists."); id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in Termops.next_global_ident_away false i (Termops.ids_of_context env) in - let env' = push_named_context ctx' env in + let env' = push_rel_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses env !isevars; let sigma = Evd.evars_of !isevars in - let substctx = Typeclasses.nf_substitution sigma subst in + let substctx = List.map (Evarutil.nf_evar sigma) subst in if Lib.is_modtype () then begin - let _, ty_constr = instance_constructor k (List.rev_map snd substctx) in + let _, ty_constr = instance_constructor k (List.rev subst) in let termtype = - let t = it_mkNamedProd_or_LetIn ty_constr ctx' in + let t = it_mkProd_or_LetIn ty_constr ctx' in Evarutil.nf_isevar !isevars t in Evarutil.check_evars env Evd.empty !isevars termtype; @@ -555,7 +399,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau end else begin - let subst, _propsctx = + let subst = let props = List.map (fun (x, l, d) -> x, Topconstr.abstract_constr_expr d (binders_of_lidents l)) @@ -567,8 +411,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau List.fold_left (fun (props, rest) (id,_,_) -> try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) @@ -579,12 +423,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau else type_ctx_instance isevars env' k.cl_props props substctx in - let app, ty_constr = instance_constructor k (List.rev_map snd subst) in + let app, ty_constr = instance_constructor k (List.rev subst) in let termtype = - let t = it_mkNamedProd_or_LetIn ty_constr ctx' in + let t = it_mkProd_or_LetIn ty_constr ctx' in Evarutil.nf_isevar !isevars t in - let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in + let term = Termops.it_mkLambda_or_LetIn app ctx' in isevars := Evarutil.nf_evar_defs !isevars; let term = Evarutil.nf_isevar !isevars term in let evm = Evd.evars_of (undefined_evars !isevars) in @@ -607,31 +451,26 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau end end -let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition - -let solve_by_tac env evd evar evi t = - let goal = {it = evi; sigma = (Evd.evars_of evd) } in - let (res, valid) = t goal in - if res.it = [] then - let prooftree = valid [] in - let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in - if obls = [] then - let evd' = evars_reset_evd res.sigma evd in - let evd' = evar_define evar proofterm evd' in - evd', true - else evd, false - else evd, false +let named_of_rel_context l = + let acc, ctx = + List.fold_right + (fun (na, b, t) (subst, ctx) -> + let id = match na with Anonymous -> raise (Invalid_argument "named_of_rel_context") | Name id -> id in + let d = (id, Option.map (substl subst) b, substl subst t) in + (mkVar id :: subst, d :: ctx)) + l ([], []) + in ctx let context ?(hook=fun _ -> ()) l = let env = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let avoid = Termops.ids_of_context env in - let ctx, l = Implicit_quantifiers.resolve_class_binders (vars_of_env env) l in - let env', avoid, ctx = interp_binders_evars isevars env avoid ctx in - let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in - isevars := Evarutil.nf_evar_defs !isevars; - let sigma = Evd.evars_of !isevars in - let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in + let evars = ref (Evd.create_evar_defs Evd.empty) in + let (env', fullctx), impls = interp_context_evars evars env l in + let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in + let ce t = Evarutil.check_evars env Evd.empty !evars t in + List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; + let ctx = try named_of_rel_context fullctx with _ -> + error "Anonymous variables not allowed in contexts." + in List.iter (function (id,_,t) -> if Lib.is_modtype () then let cst = Declare.declare_internal_constant id @@ -642,96 +481,12 @@ let context ?(hook=fun _ -> ()) l = add_instance (Typeclasses.new_instance tc None false cst); hook (ConstRef cst) | None -> () - else - (Command.declare_one_assumption false (Local (* global *), Definitional) t - [] true (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id); - match class_of_constr t with - None -> () - | Some tc -> hook (VarRef id))) - (List.rev fullctx) - -open Libobject - -let module_qualid = qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init") -let tactic_qualid = make_qualid (dirpath_of_string "Coq.Classes.Init") (id_of_string "typeclass_instantiation") - -let tactic_expr = Tacexpr.TacArg (Tacexpr.Reference (Qualid (dummy_loc, tactic_qualid))) -let tactic = lazy (Tacinterp.interp tactic_expr) - -let _ = - Typeclasses.solve_instanciation_problem := - (fun env evd ev evi -> - Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *) - solve_by_tac env evd ev evi (Lazy.force tactic)) - -(* let prod = lazy_fun Coqlib.build_prod *) - -(* let build_conjunction evm = *) -(* List.fold_left *) -(* (fun (acc, evs) (ev, evi) -> *) -(* if class_of_constr evi.evar_concl <> None then *) -(* mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs *) -(* else acc, Evd.add evs ev evi) *) -(* (Coqlib.build_coq_True (), Evd.empty) evm *) - -(* let destruct_conjunction evm_list evm evm' term = *) -(* let _, evm = *) -(* List.fold_right *) -(* (fun (ev, evi) (term, evs) -> *) -(* if class_of_constr evi.evar_concl <> None then *) -(* match kind_of_term term with *) -(* | App (x, [| _ ; _ ; proof ; term |]) -> *) -(* let evs' = Evd.define evs ev proof in *) -(* (term, evs') *) -(* | _ -> assert(false) *) -(* else *) -(* match (Evd.find evm' ev).evar_body with *) -(* Evar_empty -> raise Not_found *) -(* | Evar_defined c -> *) -(* let evs' = Evd.define evs ev c in *) -(* (term, evs')) *) -(* evm_list (term, evm) *) -(* in evm *) - -(* let solve_by_tac env evd evar evi t = *) -(* let goal = {it = evi; sigma = (Evd.evars_of evd) } in *) -(* let (res, valid) = t goal in *) -(* if res.it = [] then *) -(* let prooftree = valid [] in *) -(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *) -(* if obls = [] then *) -(* let evd' = evars_reset_evd res.sigma evd in *) -(* let evd' = evar_define evar proofterm evd' in *) -(* evd', true *) -(* else evd, false *) -(* else evd, false *) - -(* let resolve_all_typeclasses env evd = *) -(* let evm = Evd.evars_of evd in *) -(* let evm_list = Evd.to_list evm in *) -(* let goal, typesevm = build_conjunction evm_list in *) -(* let evars = ref (Evd.create_evar_defs typesevm) in *) -(* let term = resolve_one_typeclass_evd env evars goal in *) -(* let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in *) -(* Evd.create_evar_defs evm' *) - -(* let _ = *) -(* Typeclasses.solve_instanciations_problem := *) -(* (fun env evd -> *) -(* Library.require_library [(dummy_loc, module_qualid)] None; (\* may be inefficient *\) *) -(* resolve_all_typeclasses env evd) *) - -let solve_evars_by_tac env evd t = - let ev = make_evar empty_named_context_val mkProp in - let goal = {it = ev; sigma = (Evd.evars_of evd) } in - let (res, valid) = t goal in - let evd' = evars_reset_evd res.sigma evd in - evd' -(* Library.require_library [(dummy_loc, module_qualid)] None (a\* may be inefficient *\); *) - -(* let _ = *) -(* Typeclasses.solve_instanciations_problem := *) -(* (fun env evd -> *) -(* Eauto.resolve_all_evars false (true, 15) env *) -(* (fun ev evi -> is_implicit_arg (snd (evar_source ev evd)) *) -(* && class_of_constr evi.evar_concl <> None) evd) *) + else ( + let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + in + Command.declare_one_assumption false (Local (* global *), Definitional) t + [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id); + match class_of_constr t with + | None -> () + | Some tc -> hook (VarRef id))) + (List.rev ctx) |