diff options
Diffstat (limited to 'plugins/subtac/subtac_classes.ml')
| -rw-r--r-- | plugins/subtac/subtac_classes.ml | 39 |
1 files changed, 22 insertions, 17 deletions
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 960bf162..c08dd16d 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -1,19 +1,16 @@ -(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pretyping open Evd open Environ open Term -open Rawterm +open Glob_term open Topconstr open Names open Libnames @@ -23,24 +20,28 @@ open Constrintern open Subtac_command open Typeclasses open Typeclasses_errors -open Termops open Decl_kinds open Entries open Util module SPretyping = Subtac_pretyping.Pretyping -let interp_constr_evars_gen evdref env ?(impls=[]) kind c = +let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c = SPretyping.understand_tcc_evars evdref env kind - (intern_gen (kind=IsType) ~impls ( !evdref) env c) + (intern_gen (kind=IsType) ~impls !evdref env c) -let interp_casted_constr_evars evdref env ?(impls=[]) c typ = +let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c let interp_context_evars evdref env params = - Constrintern.interp_context_gen + let impls_env, bl = Constrintern.interp_context_gen (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t) - (SPretyping.understand_judgment_tcc evdref) !evdref env params + (SPretyping.understand_judgment_tcc evdref) !evdref env params in bl + +let interp_type_evars_impls ~evdref ?(impls=empty_internalization_env) env c = + let c = intern_gen true ~impls !evdref env c in + let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in + SPretyping.understand_tcc_evars ~fail_evar:false evdref env IsType c, imps let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function @@ -113,11 +114,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let subst = List.map (Evarutil.nf_evar sigma) subst in let props = match props with - | CRecord (loc, _, fs) -> + | Some (CRecord (loc, _, fs)) -> if List.length fs > List.length k.cl_props then Classes.mismatched_props env' (List.map snd fs) k.cl_props; Inl fs - | _ -> Inr props + | Some p -> Inr p + | None -> Inl [] in let subst = match props with @@ -138,7 +140,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in let (loc, mid) = get_id loc_mid in - Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); + List.iter + (fun (n, _, x) -> + if n = Name mid then + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) + k.cl_projs; c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest @@ -173,10 +179,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p Evarutil.check_evars env Evd.empty !evars termtype; let hook vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in - let inst = Typeclasses.new_instance k pri global (ConstRef cst) in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; - Typeclasses.add_instance inst + Typeclasses.declare_instance pri (not global) (ConstRef cst) in let evm = Subtac_utils.evars_of_term !evars Evd.empty term in let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in - id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls + id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls |