diff options
30 files changed, 317 insertions, 168 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 239d28133..fa0e2fe52 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -201,7 +201,7 @@ GEXTEND Gram [ [ "fun" -> () ] ] ; record_declaration: - [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs) + [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (loc, None, fs) (* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) (* CRecord (loc, Some c, fs) *) ] ] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 72a2ba198..15f81c723 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -560,8 +560,8 @@ GEXTEND Gram | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] ; - props = [ ":="; "{"; r = record_declaration; "}" -> r | - ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> + props = [ ":="; "{"; r = record_declaration; "}" -> Some r | + ":="; c = lconstr -> Some c | -> None ] -> VernacInstance (false, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), props, pri) @@ -633,7 +633,7 @@ GEXTEND Gram pri = OPT [ "|"; i = natural -> i ] -> VernacInstance (true, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), - CRecord (loc, None, []), pri) + None, pri) (* System directory *) | IDENT "Pwd" -> VernacChdir None diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 956d7eb06..9578dc7ce 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -699,8 +699,9 @@ let rec pr_vernac = function str"=>" ++ spc () ++ (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++ pr_constr_expr cl ++ spc () ++ - spc () ++ str":=" ++ spc () ++ - pr_constr_expr props) + (match props with + | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr_expr p + | None -> mt())) | VernacContext l -> hov 1 ( diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 419205a19..05e634c58 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -109,11 +109,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 diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli index c7687abf3..5b5c02037 100644 --- a/plugins/subtac/subtac_classes.mli +++ b/plugins/subtac/subtac_classes.mli @@ -33,7 +33,7 @@ val new_instance : ?global:bool -> local_binder list -> typeclass_constraint -> - constr_expr -> + constr_expr option -> ?generalize:bool -> int option -> identifier * Subtac_obligations.progress diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c5bcb631e..6e92d74ab 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -36,8 +36,6 @@ let flex_kind_of_term c l = | Meta _ | Case _ | Fix _ -> PseudoRigid c | Cast _ | App _ -> assert false -let is_rigid = function Rigid _ -> true | _ -> false - let eval_flexible_term ts env c = match kind_of_term c with | Const c -> @@ -200,7 +198,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have flushed evars *) match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with - | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = if List.length l1 > List.length l2 then diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index cca7aee1d..eabef3641 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -32,10 +32,10 @@ let register_remove_instance_hint = (:=) remove_instance_hint_ref let remove_instance_hint id = !remove_instance_hint_ref id -let set_typeclass_transparency_ref = ref (fun id pri -> assert false) +let set_typeclass_transparency_ref = ref (fun id local c -> assert false) let register_set_typeclass_transparency = (:=) set_typeclass_transparency_ref -let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c +let set_typeclass_transparency gr local c = !set_typeclass_transparency_ref gr local c type rels = constr list @@ -200,7 +200,11 @@ let discharge_class (_,cl) = cl_props = props; cl_projs = list_smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs } -let rebuild_class cl = cl +let rebuild_class cl = + try + let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in + set_typeclass_transparency cst false false; cl + with _ -> cl let class_input = declare_object @@ -305,7 +309,7 @@ let add_constant_class cst = cl_projs = [] } in add_class tc; - set_typeclass_transparency (EvalConstRef cst) false + set_typeclass_transparency (EvalConstRef cst) false false let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 1fe955b0c..77567bece 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -87,8 +87,8 @@ val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : env -> evar_map -> types -> open_constr -val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit -val set_typeclass_transparency : evaluable_global_reference -> bool -> unit +val register_set_typeclass_transparency : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) -> unit +val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit val register_add_instance_hint : (global_reference -> bool (* local? *) -> int option -> unit) -> unit val register_remove_instance_hint : (global_reference -> unit) -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5982de65e..7b01134e0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -168,6 +168,7 @@ type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly : bool; modulo_delta : Names.transparent_state; + modulo_delta_types : Names.transparent_state; resolve_evars : bool; use_evars_pattern_unification : bool; modulo_eta : bool @@ -177,6 +178,7 @@ let default_unify_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; modulo_delta = full_transparent_state; + modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = true; modulo_eta = true @@ -186,6 +188,7 @@ let default_no_delta_unify_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = false; modulo_eta = true @@ -574,10 +577,12 @@ let applyHead env evd n c = in apprec n c (Typing.type_of env evd c) evd -let is_mimick_head f = +let is_mimick_head ts f = match kind_of_term f with - (Const _|Var _|Rel _|Construct _|Ind _) -> true - | _ -> false + | Const c -> not (Closure.is_transparent_constant ts c) + | Var id -> not (Closure.is_transparent_variable ts id) + | (Rel _|Construct _|Ind _) -> true + | _ -> false let try_to_coerce env evd c cty tycon = let j = make_judge c cty in @@ -663,18 +668,18 @@ let w_merge env with_types flags (evd,metas,evars) = | App (f,cl) when occur_meta rhs' -> if occur_evar evk rhs' then error_occur_check curenv evd evk rhs'; - if is_mimick_head f then + if is_mimick_head flags.modulo_delta f then let evd' = mimick_undefined_evar evd flags f (Array.length cl) evk in w_merge_rec evd' metas evars eqns else let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in - w_merge_rec (solve_simple_evar_eqn flags.modulo_delta curenv evd' ev rhs'') + w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'') metas evars' eqns | _ -> let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in - w_merge_rec (solve_simple_evar_eqn flags.modulo_delta curenv evd' ev rhs'') + w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'') metas evars' eqns end | [] -> diff --git a/pretyping/unification.mli b/pretyping/unification.mli index cc3040a9e..0462688b4 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -14,6 +14,7 @@ type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly : bool; modulo_delta : Names.transparent_state; + modulo_delta_types : Names.transparent_state; resolve_evars : bool; use_evars_pattern_unification : bool; modulo_eta : bool @@ -49,3 +50,11 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> (exported for inv.ml) *) val abstract_list_all : env -> evar_map -> constr -> constr -> constr list -> constr + + +(* For tracing *) + +val w_merge : env -> bool -> unify_flags -> evar_map * + (metavariable * constr * (instance_constraint * instance_typing_status)) list * + (env * types pexistential * types) list -> evar_map + diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 76f3856e3..13eda9156 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -105,6 +105,7 @@ let fail_quick_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = false; modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = false; modulo_eta = true diff --git a/tactics/auto.ml b/tactics/auto.ml index b48e8fbc8..daedd9892 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -173,9 +173,14 @@ module Hint_db = struct | Give_exact _ -> true | _ -> false + let is_unfold = function + | Unfold_nth _ -> true + | _ -> false + let addkv gr v db = let k = match gr with - | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr then None else Some gr + | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && + is_unfold v.code then None else Some gr | None -> None in let dnst = if db.use_dn then Some db.hintdb_state else None in @@ -268,6 +273,9 @@ let current_db_names () = (**************************************************************************) let auto_init : (unit -> unit) ref = ref (fun () -> ()) +let add_auto_init f = + let init = !auto_init in + auto_init := (fun () -> init (); f ()) let init () = searchtable := Hintdbmap.empty; !auto_init () let freeze () = !searchtable @@ -834,6 +842,7 @@ let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = false; modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; resolve_evars = true; use_evars_pattern_unification = false; modulo_eta = true diff --git a/tactics/auto.mli b/tactics/auto.mli index 1bc321c94..69568d4f8 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -247,4 +247,4 @@ val superauto : int -> (identifier * constr) list -> autoArguments list -> tacti val h_superauto : int option -> reference list -> bool -> bool -> tactic -val auto_init : (unit -> unit) ref +val add_auto_init : (unit -> unit) -> unit diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index d17c783e9..cfc18e232 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -40,8 +40,9 @@ open Compat let default_eauto_depth = 100 let typeclasses_db = "typeclass_instances" -let _ = Auto.auto_init := (fun () -> - Auto.create_hint_db false typeclasses_db full_transparent_state true) +let _ = + Auto.add_auto_init + (fun () -> Auto.create_hint_db false typeclasses_db full_transparent_state true) exception Found of evar_map @@ -74,6 +75,7 @@ let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; modulo_delta = var_full_transparent_state; + modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = true; modulo_eta = true @@ -125,7 +127,9 @@ let with_prods nprods (c, clenv) f gls = let flags_of_state st = {auto_unif_flags with - modulo_conv_on_closed_terms = Some st; modulo_delta = st; modulo_eta = false} + modulo_conv_on_closed_terms = Some st; modulo_delta = st; + modulo_delta_types = st; + modulo_eta = false} let rec e_trivial_fail_db db_list local_db goal = let tacl = @@ -285,63 +289,117 @@ let compare (pri, _, _, res) (pri', _, _, res') = let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls } +(* let hints_tac hints = *) +(* { skft = fun sk fk {it = gl,info; sigma = s} -> *) +(* let possible_resolve (lgls as res, pri, b, pp) = *) +(* (pri, pp, b, res) *) +(* in *) +(* let tacs = *) +(* let concl = Goal.V82.concl s gl in *) +(* let poss = e_possible_resolve hints info.hints concl in *) +(* let l = *) +(* let tacgl = {it = gl; sigma = s} in *) +(* Util.list_map_append (fun (tac, pri, b, pptac) -> *) +(* try [tac tacgl, pri, b, pptac] with e when catchable e -> []) *) +(* poss *) +(* in *) +(* if l = [] && !typeclasses_debug then *) +(* msgnl (pr_depth info.auto_depth ++ str": no match for " ++ *) +(* Printer.pr_constr_env (Goal.V82.env s gl) concl ++ *) +(* spc () ++ int (List.length poss) ++ str" possibilities"); *) +(* List.map possible_resolve l *) +(* in *) +(* let tacs = List.sort compare tacs in *) +(* let rec aux i = function *) +(* | (_, pp, b, {it = gls; sigma = s'}) :: tl -> *) +(* if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp *) +(* ++ str" on" ++ spc () ++ pr_ev s gl); *) +(* let fk = *) +(* (fun () -> (\* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *\) *) +(* aux (succ i) tl) *) +(* in *) +(* let sgls = *) +(* evars_to_goals (fun evm ev evi -> *) +(* if Typeclasses.is_resolvable evi && *) +(* (not info.only_classes || Typeclasses.is_class_evar evm evi) *) +(* then Typeclasses.mark_unresolvable evi, true *) +(* else evi, false) s' *) +(* in *) +(* let newgls, s' = *) +(* let gls' = List.map (fun g -> (None, g)) gls in *) +(* match sgls with *) +(* | None -> gls', s' *) +(* | Some (evgls, s') -> *) +(* (gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s') *) +(* in *) +(* let gls' = list_map_i (fun j (evar, g) -> *) +(* let info = *) +(* { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp; *) +(* is_evar = evar; *) +(* hints = *) +(* if b && Goal.V82.hyps s' g <> Goal.V82.hyps s' gl *) +(* then make_autogoal_hints info.only_classes *) +(* ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'} *) +(* else info.hints } *) +(* in g, info) 1 newgls in *) +(* let glsv = {it = gls'; sigma = s'} in *) +(* sk glsv fk *) +(* | [] -> fk () *) +(* in aux 1 tacs } *) + let hints_tac hints = { skft = fun sk fk {it = gl,info; sigma = s} -> - let possible_resolve (lgls as res, pri, b, pp) = - (pri, pp, b, res) - in - let tacs = let concl = Goal.V82.concl s gl in + let tacgl = {it = gl; sigma = s} in let poss = e_possible_resolve hints info.hints concl in - let l = - let tacgl = {it = gl; sigma = s} in - Util.list_map_append (fun (tac, pri, b, pptac) -> - try [tac tacgl, pri, b, pptac] with e when catchable e -> []) - poss - in - if l = [] && !typeclasses_debug then - msgnl (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_constr_env (Goal.V82.env s gl) concl ++ - spc () ++ int (List.length poss) ++ str" possibilities"); - List.map possible_resolve l - in - let tacs = List.sort compare tacs in - let rec aux i = function - | (_, pp, b, {it = gls; sigma = s'}) :: tl -> - if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev s gl); - let fk = - (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *) - aux (succ i) tl) - in - let sgls = - evars_to_goals (fun evm ev evi -> - if Typeclasses.is_resolvable evi && - (not info.only_classes || Typeclasses.is_class_evar evm evi) - then Typeclasses.mark_unresolvable evi, true - else evi, false) s' - in - let newgls, s' = - let gls' = List.map (fun g -> (None, g)) gls in - match sgls with - | None -> gls', s' - | Some (evgls, s') -> - (gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s') - in - let gls' = list_map_i (fun j (evar, g) -> - let info = - { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp; - is_evar = evar; - hints = - if b && Goal.V82.hyps s' g <> Goal.V82.hyps s' gl - then make_autogoal_hints info.only_classes - ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'} - else info.hints } - in g, info) 1 newgls in - let glsv = {it = gls'; sigma = s'} in - sk glsv fk - | [] -> fk () - in aux 1 tacs } + let rec aux i foundone = function + | (tac, _, b, pp) :: tl -> + let res = try Some (tac tacgl) with e when catchable e -> None in + (match res with + | None -> aux (succ i) foundone tl + | Some {it = gls; sigma = s'} -> + if !typeclasses_debug then + msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp + ++ str" on" ++ spc () ++ pr_ev s gl); + let fk = + (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *) + aux (succ i) true tl) + in + let sgls = + evars_to_goals + (fun evm ev evi -> + if Typeclasses.is_resolvable evi && + (not info.only_classes || Typeclasses.is_class_evar evm evi) + then Typeclasses.mark_unresolvable evi, true + else evi, false) s' + in + let newgls, s' = + let gls' = List.map (fun g -> (None, g)) gls in + match sgls with + | None -> gls', s' + | Some (evgls, s') -> + (gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s') + in + let gls' = list_map_i + (fun j (evar, g) -> + let info = + { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp; + is_evar = evar; + hints = + if b && Goal.V82.hyps s' g <> Goal.V82.hyps s' gl + then make_autogoal_hints info.only_classes + ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'} + else info.hints } + in g, info) 1 newgls in + let glsv = {it = gls'; sigma = s'} in + sk glsv fk) + | [] -> + if not foundone && !typeclasses_debug then + msgnl (pr_depth info.auto_depth ++ str": no match for " ++ + Printer.pr_constr_env (Goal.V82.env s gl) concl ++ + spc () ++ int (List.length poss) ++ str" possibilities"); + fk () + in aux 1 false poss } let dependent only_classes evd oev concl = if oev <> None then true @@ -602,7 +660,7 @@ let set_transparency cl b = List.iter (fun r -> let gr = Smartlocate.global_with_alias r in let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in - Classes.set_typeclass_transparency ev b) cl + Classes.set_typeclass_transparency ev false b) cl VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ diff --git a/tactics/equality.ml b/tactics/equality.ml index 079a18c1e..40514a28f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -84,6 +84,7 @@ let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; Unification.use_metas_eagerly = true; Unification.modulo_delta = empty_transparent_state; + Unification.modulo_delta_types = empty_transparent_state; Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; Unification.modulo_eta = true diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index df79bf3ee..9ad419697 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -224,6 +224,7 @@ type hypinfo = { c2 : constr; c : (Tacinterp.interp_sign * Genarg.glob_constr_and_expr with_bindings) option; abs : (constr * types) option; + flags : Unification.unify_flags; } let goalevars evars = fst evars @@ -251,7 +252,7 @@ let rec decompose_app_rel env evd t = (* let nc, c', cl = push_rel_context_to_named_context env c in *) (* let env' = reset_with_named_context nc env in *) -let decompose_applied_relation env sigma orig (c,l) left2right = +let decompose_applied_relation env sigma flags orig (c,l) left2right = let c' = c in let ctype = Typing.type_of env sigma c' in let find_rel ty = @@ -265,7 +266,8 @@ let decompose_applied_relation env sigma orig (c,l) left2right = else Some { cl=eqclause; prf=(Clenv.clenv_value eqclause); car=ty1; rel = equiv; - l2r=left2right; c1=c1; c2=c2; c=orig; abs=None } + l2r=left2right; c1=c1; c2=c2; c=orig; abs=None; + flags = flags } in match find_rel ctype with | Some c -> c @@ -276,30 +278,52 @@ let decompose_applied_relation env sigma orig (c,l) left2right = | None -> error "The term does not end with an applied homogeneous relation." open Tacinterp -let decompose_applied_relation_expr env sigma (is, (c,l)) left2right = +let decompose_applied_relation_expr env sigma flags (is, (c,l)) left2right = let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in - decompose_applied_relation env sigma (Some (is, (c,l))) cbl left2right - -let rewrite_unif_flags = { - Unification.modulo_conv_on_closed_terms = None; - Unification.use_metas_eagerly = true; - Unification.modulo_delta = empty_transparent_state; - Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; - Unification.modulo_eta = true -} + decompose_applied_relation env sigma flags (Some (is, (c,l))) cbl left2right + +let rewrite_db = "rewrite" let conv_transparent_state = (Idpred.empty, Cpred.full) -let rewrite2_unif_flags = { - Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; +let _ = + Auto.add_auto_init + (fun () -> + Auto.create_hint_db false rewrite_db conv_transparent_state true) + +let rewrite_transparent_state () = + Auto.Hint_db.transparent_state (Auto.searchtable_map rewrite_db) + +let rewrite_unif_flags = { + Unification.modulo_conv_on_closed_terms = None; Unification.use_metas_eagerly = true; Unification.modulo_delta = empty_transparent_state; + Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; Unification.modulo_eta = true } +let rewrite2_unif_flags = + { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; + Unification.use_metas_eagerly = true; + Unification.modulo_delta = empty_transparent_state; + Unification.modulo_delta_types = conv_transparent_state; + Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; + Unification.modulo_eta = true + } + +let general_rewrite_unif_flags () = + let ts = rewrite_transparent_state () in + { Unification.modulo_conv_on_closed_terms = Some ts; + Unification.use_metas_eagerly = true; + Unification.modulo_delta = ts; + Unification.modulo_delta_types = ts; + Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; + Unification.modulo_eta = true } + let convertible env evd x y = Reductionops.is_conv env evd x y @@ -307,11 +331,11 @@ let allowK = true let refresh_hypinfo env sigma hypinfo = if hypinfo.abs = None then - let {l2r=l2r; c=c;cl=cl} = hypinfo in + let {l2r=l2r; c=c;cl=cl;flags=flags} = hypinfo in match c with | Some c -> (* Refresh the clausenv to not get the same meta twice in the goal. *) - decompose_applied_relation_expr env sigma c l2r; + decompose_applied_relation_expr env sigma flags c l2r; | _ -> hypinfo else hypinfo @@ -327,10 +351,7 @@ let unify_eqn env sigma hypinfo t = env', prf, c1, c2, car, rel | None -> let env' = - try clenv_unify allowK ~flags:rewrite_unif_flags CONV left t cl - with Pretype_errors.PretypeError _ -> - (* For Ring essentially, only when doing setoid_rewrite *) - clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl + clenv_unify allowK ~flags:!hypinfo.flags CONV left t cl in let env' = Clenvtac.clenv_pose_dependent_evars true env' in (* let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *) @@ -610,9 +631,9 @@ let apply_rule hypinfo loccs : strategy = end | _ -> None -let apply_lemma (evm,c) left2right loccs : strategy = +let apply_lemma flags (evm,c) left2right loccs : strategy = fun env avoid t ty cstr evars -> - let hypinfo = ref (decompose_applied_relation env (goalevars evars) None c left2right) in + let hypinfo = ref (decompose_applied_relation env (goalevars evars) flags None c left2right) in apply_rule hypinfo loccs env avoid t ty cstr evars let make_leibniz_proof c ty r = @@ -852,7 +873,7 @@ let subterm all flags (s : strategy) : strategy = rew_from = t; rew_to = unfold_match env (goalevars evars) cst prf.rew_to }) | x' -> x) - | _ -> if all then Some None else None + | _ -> None in aux let all_subterms = subterm true default_flags @@ -950,22 +971,24 @@ module Strategies = let outermost (s : strategy) : strategy = fix (fun out -> choice s (one_subterm out)) - let lemmas cs : strategy = + let lemmas flags cs : strategy = List.fold_left (fun tac (l,l2r) -> - choice tac (apply_lemma l l2r (false,[]))) + choice tac (apply_lemma flags l l2r (false,[]))) fail cs let inj_open c = (Evd.empty,c) let old_hints (db : string) : strategy = let rules = Autorewrite.find_rewrites db in - lemmas (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules) + lemmas rewrite_unif_flags + (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules) let hints (db : string) : strategy = fun env avoid t ty cstr evars -> let rules = Autorewrite.find_matches db t in - lemmas (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules) - env avoid t ty cstr evars + let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r) in + let lems = List.map lemma rules in + lemmas rewrite_unif_flags lems env avoid t ty cstr evars let reduce (r : Redexpr.red_expr) : strategy = let rfn, ckind = Redexpr.reduction_of_red_expr r in @@ -1009,10 +1032,10 @@ let get_hypinfo_ids {c = opt} = | None -> [] | Some (is, gc) -> List.map fst is.lfun @ is.avoid_ids -let rewrite_with c left2right loccs : strategy = +let rewrite_with flags c left2right loccs : strategy = fun env avoid t ty cstr evars -> let gevars = goalevars evars in - let hypinfo = ref (decompose_applied_relation_expr env gevars c left2right) in + let hypinfo = ref (decompose_applied_relation_expr env gevars flags c left2right) in let avoid = get_hypinfo_ids !hypinfo @ avoid in rewrite_strat default_flags loccs hypinfo env avoid t ty cstr (gevars, cstrevars evars) @@ -1238,7 +1261,7 @@ let cl_rewrite_clause_new_strat ?abs strat clause = let cl_rewrite_clause_newtac' l left2right occs clause = Proof_global.run_tactic (Proofview.tclFOCUS 1 1 - (cl_rewrite_clause_new_strat (rewrite_with l left2right occs) clause)) + (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)) let cl_rewrite_clause_strat strat clause gl = init_setoid (); @@ -1249,7 +1272,7 @@ let cl_rewrite_clause_strat strat clause gl = tclFAIL 0 (str"setoid rewrite failed: strategy failed") gl let cl_rewrite_clause l left2right occs clause gl = - cl_rewrite_clause_strat (rewrite_with l left2right occs) clause gl + cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl open Pp open Pcoq @@ -1269,7 +1292,8 @@ let occurrences_of = function let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars -> let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in - apply_lemma (evd, (c, NoBindings)) l2r occs env avoid t ty cstr (evd, cstrevars evars) + apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) + l2r occs env avoid t ty cstr (evd, cstrevars evars) let interp_constr_list env sigma = List.map (fun c -> @@ -1348,7 +1372,7 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy | [ "old_hints" preident(h) ] -> [ Strategies.old_hints h ] | [ "hints" preident(h) ] -> [ Strategies.hints h ] | [ "terms" constr_list(h) ] -> [ fun env avoid t ty cstr evars -> - Strategies.lemmas (interp_constr_list env (goalevars evars) h) env avoid t ty cstr evars ] + Strategies.lemmas rewrite_unif_flags (interp_constr_list env (goalevars evars) h) env avoid t ty cstr evars ] | [ "eval" red_expr(r) ] -> [ fun env avoid t ty cstr evars -> Strategies.reduce (Tacinterp.interp_redexp env (goalevars evars) r) env avoid t ty cstr evars ] | [ "fold" constr(c) ] -> [ Strategies.fold c ] @@ -1414,7 +1438,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance binders instance (CRecord (dummy_loc,None,fields)) + new_instance binders instance (Some (CRecord (dummy_loc,None,fields))) ~global:(not (Vernacexpr.use_section_locality ())) ~generalize:false None let declare_instance_refl global binders a aeq n lemma = @@ -1686,7 +1710,7 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in - ignore(new_instance ~global:glob binders instance (CRecord (dummy_loc,None,[])) + ignore(new_instance ~global:glob binders instance (Some (CRecord (dummy_loc,None,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) VERNAC COMMAND EXTEND AddSetoid1 @@ -1728,7 +1752,7 @@ let check_evar_map_of_evars_defs evd = check_freemetas_is_empty rebus2 freemetas2 ) metas -let unification_rewrite l2r c1 c2 cl car rel but gl = +let unification_rewrite flags l2r c1 c2 cl car rel but gl = let env = pf_env gl in let (evd',c') = try @@ -1740,7 +1764,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = Pretype_errors.PretypeError _ -> (* ~flags:(true,true) to make Ring work (since it really exploits conversion) *) - Unification.w_unify_to_subterm ~flags:rewrite2_unif_flags + Unification.w_unify_to_subterm ~flags:flags env ((if l2r then c1 else c2),but) cl.evd in let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in @@ -1753,15 +1777,18 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = check_evar_map_of_evars_defs cl'.evd; let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in - {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)} + {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty); + flags = flags} let get_hyp gl evars (c,l) clause l2r = - let hi = decompose_applied_relation (pf_env gl) evars None (c,l) l2r in + let flags = rewrite2_unif_flags in + let hi = decompose_applied_relation (pf_env gl) evars flags None (c,l) l2r in let but = match clause with | Some id -> pf_get_hyp_typ gl id | None -> Evarutil.nf_evar evars (pf_concl gl) in - unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl + { unification_rewrite flags hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl with + flags = rewrite_unif_flags } let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } @@ -1912,3 +1939,35 @@ TACTIC EXTEND fold_matches let c' = fold_matches (pf_env gl) (project gl) c in change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ] END + +TACTIC EXTEND myapply +| [ "myapply" global(id) constr_list(l) ] -> [ + fun gl -> + let gr = id in + let _, impls = List.hd (Impargs.implicits_of_global gr) in + let ty = Global.type_of_global gr in + let env = pf_env gl in + let evars = ref (project gl) in + let app = + let rec aux ty impls args args' = + match impls, kind_of_term ty with + | Some (_, _, (_, _)) :: impls, Prod (n, t, t') -> + let arg = Evarutil.e_new_evar evars env t in + aux (subst1 arg t') impls args (arg :: args') + | None :: impls, Prod (n, t, t') -> + (match args with + | [] -> + if dependent (mkRel 1) t' then + let arg = Evarutil.e_new_evar evars env t in + aux (subst1 arg t') impls args (arg :: args') + else + let arg = Evarutil.mk_new_meta () in + evars := meta_declare (destMeta arg) t !evars; + aux (subst1 arg t') impls args (arg :: args') + | arg :: args -> + aux (subst1 arg t') impls args (arg :: args')) + | _, _ -> mkApp (constr_of_global gr, Array.of_list (List.rev args')) + in aux ty impls l [] + in + tclTHEN (Refiner.tclEVARS !evars) (apply app) gl ] +END diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0ad64c21c..cd618ed98 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -700,6 +700,7 @@ let elim_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = true; modulo_eta = true @@ -894,7 +895,7 @@ let descend_in_conjunctions tac exit c gl = | Some (p,pt) -> tclTHENS (internal_cut id pt) - [refine_no_check p; + [refine p; (* Might be ill-typed due to forbidden elimination. *) tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl) n) gl | None -> diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 7972c96ca..0fa5bfaa6 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -88,10 +88,10 @@ Section RelCompFun_Instances. `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f). Proof. firstorder. Qed. - Global Instance RelCompFun_Equivalence + Global Program Instance RelCompFun_Equivalence `(Measure A B f, Equivalence _ R) : Equivalence (R@@f). - Global Instance RelCompFun_StrictOrder + Global Program Instance RelCompFun_StrictOrder `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f). End RelCompFun_Instances. @@ -108,7 +108,7 @@ Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B) `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). Proof. firstorder. Qed. -Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) +Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). Lemma FstRel_ProdRel {A B}(RA:relation A) : diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index c81a72f89..206714949 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -494,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). - Global Instance eqk_equiv : Equivalence eq_key. - Global Instance eqke_equiv : Equivalence eq_key_elt. - Global Instance ltk_strorder : StrictOrder lt_key. + Global Program Instance eqk_equiv : Equivalence eq_key. + Global Program Instance eqke_equiv : Equivalence eq_key_elt. + Global Program Instance ltk_strorder : StrictOrder lt_key. Lemma mem_find : forall m x, mem x m = match find x m with None => false | _ => true end. diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index c3d614eeb..6b3d86d39 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -264,7 +264,7 @@ Module Update_WSets Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In. Proof. intros x x' Hx s s' Hs. subst. apply MF.In_eq_iff; auto. Qed. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Section Spec. Variable s s': t. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 851237d8f..20504bcf8 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -872,7 +872,7 @@ Module MakeListOrdering (O:OrderedType). Definition eq s s' := forall x, In x s <-> In x s'. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Inductive lt_list : t -> t -> Prop := | lt_nil : forall x s, lt_list nil (x :: s) diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 799e5f57e..76f09c76e 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -515,7 +515,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Definition In := InA X.eq. Definition eq := Equal. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. End MakeRaw. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index 2bdc1bba2..a4f0dbce1 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -115,7 +115,7 @@ Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy. Local Obligation Tactic := solve_wd2 || solve_wd1. Instance : Measure to_Q. -Instance eq_equiv : Equivalence eq. +Instance eq_equiv : Equivalence eq := {}. Program Instance lt_wd : Proper (eq==>eq==>iff) lt. Program Instance le_wd : Proper (eq==>eq==>iff) le. @@ -141,7 +141,7 @@ Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed. (** Let's implement [TotalOrder] *) Definition lt_compat := lt_wd. -Instance lt_strorder : StrictOrder lt. +Instance lt_strorder : StrictOrder lt := {}. Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. Proof. intros. qify. apply Qle_lteq. Qed. diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index d8a1b7581..c69885b46 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -29,9 +29,9 @@ Module KeyDecidableType(Import D:DecidableType). (* eqk, eqke are equalities, ltk is a strict order *) - Global Instance eqk_equiv : Equivalence eqk. + Global Instance eqk_equiv : Equivalence eqk := _. - Global Instance eqke_equiv : Equivalence eqke. + Global Instance eqke_equiv : Equivalence eqke := _. (* Additionnal facts *) @@ -143,7 +143,7 @@ Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. Definition eq := (D1.eq * D2.eq)%signature. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. @@ -159,7 +159,7 @@ End PairDecidableType. Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := (D1.t * D2.t)%type. Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. intros (x1,x2) (y1,y2); diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index a28b79776..b328ae2e8 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -208,7 +208,7 @@ Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull. Definition t := O.t. Definition eq := O.eq. -Instance eq_equiv : Equivalence eq. +Program Instance eq_equiv : Equivalence eq. Definition eq_dec := O.eq_dec. Definition lt := flip O.lt. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 2ed070268..f83b63779 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -86,11 +86,11 @@ Module KeyOrderedType(Import O:OrderedType). (* eqk, eqke are equalities, ltk is a strict order *) - Global Instance eqk_equiv : Equivalence eqk. + Global Instance eqk_equiv : Equivalence eqk := _. - Global Instance eqke_equiv : Equivalence eqke. + Global Instance eqke_equiv : Equivalence eqke := _. - Global Instance ltk_strorder : StrictOrder ltk. + Global Instance ltk_strorder : StrictOrder ltk := _. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. unfold eqk, ltk; auto with *. Qed. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 2f0bb480f..4f1df4bb9 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -30,8 +30,8 @@ open Entries let typeclasses_db = "typeclass_instances" -let set_typeclass_transparency c b = - Auto.add_hints false [typeclasses_db] +let set_typeclass_transparency c local b = + Auto.add_hints local [typeclasses_db] (Auto.HintsTransparencyEntry ([c], b)) let _ = @@ -186,18 +186,20 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props begin let props = match props with - | CRecord (loc, _, fs) -> + | Some (CRecord (loc, _, fs)) -> if List.length fs > List.length k.cl_props then mismatched_props env' (List.map snd fs) k.cl_props; - Inl fs - | _ -> Inr props + Some (Inl fs) + | Some t -> Some (Inr t) + | None -> None in let subst = match props with - | Inr term -> + | None -> if k.cl_props = [] then Some (Inl subst) else None + | Some (Inr term) -> let c = interp_casted_constr_evars evars env' term cty in - Inr (c, subst) - | Inl props -> + Some (Inr (c, subst)) + | Some (Inl props) -> let get_id = function | Ident id' -> id' @@ -224,12 +226,14 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if rest <> [] then unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) else - Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) + Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)) in evars := Evarutil.nf_evar_map !evars; let term, termtype = match subst with - | Inl subst -> + | None -> let termtype = it_mkProd_or_LetIn cty ctx in + None, termtype + | Some (Inl subst) -> let subst = List.fold_left2 (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') [] subst (k.cl_props @ snd k.cl_context) @@ -237,26 +241,25 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let app, ty_constr = instance_constructor k subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in - term, termtype - | Inr (def, subst) -> + Some term, termtype + | Some (Inr (def, subst)) -> let termtype = it_mkProd_or_LetIn cty ctx in let term = Termops.it_mkLambda_or_LetIn def ctx in - term, termtype + Some term, termtype in let termtype = Evarutil.nf_evar !evars termtype in - let term = Evarutil.nf_evar !evars term in + let term = Option.map (Evarutil.nf_evar !evars) term in let evm = undefined_evars !evars in Evarutil.check_evars env Evd.empty !evars termtype; - if Evd.is_empty evm then - declare_instance_constant k pri global imps ?hook id term termtype + if Evd.is_empty evm && term <> None then + declare_instance_constant k pri global imps ?hook id (Option.get term) termtype else begin evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); - if props <> Inl [] then - Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *) - (!refine_ref (evm, term)) + if term <> None then + Pfedit.by (!refine_ref (evm, Option.get term)) else if Flags.is_auto_intros () then Pfedit.by (Refiner.tclDO len Tactics.intro); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); diff --git a/toplevel/classes.mli b/toplevel/classes.mli index bc0eb89c0..b57f1bea0 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -50,7 +50,7 @@ val new_instance : ?global:bool -> (** Not global by default. *) local_binder list -> typeclass_constraint -> - constr_expr -> + constr_expr option -> ?generalize:bool -> ?tac:Proof_type.tactic -> ?hook:(Libnames.global_reference -> unit) -> @@ -59,7 +59,7 @@ val new_instance : (** Setting opacity *) -val set_typeclass_transparency : evaluable_global_reference -> bool -> unit +val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit (** For generation on names based on classes only *) diff --git a/toplevel/record.ml b/toplevel/record.ml index ae09d080f..36d29c1a1 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -329,7 +329,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let cref = ConstRef cst in Impargs.declare_manual_implicits false cref [paramimpls]; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - Classes.set_typeclass_transparency (EvalConstRef cst) false; + Classes.set_typeclass_transparency (EvalConstRef cst) false false; if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); cref, [Name proj_name, List.hd coers, Some proj_cst] | _ -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 3b9bf9a55..6858de706 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -255,7 +255,7 @@ type vernac_expr = bool * (* global *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) - constr_expr * (* props *) + constr_expr option * (* props *) int option (* Priority *) | VernacContext of local_binder list |