aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_vernac.ml46
-rw-r--r--parsing/ppvernac.ml5
-rw-r--r--plugins/subtac/subtac_classes.ml5
-rw-r--r--plugins/subtac/subtac_classes.mli2
-rw-r--r--pretyping/evarconv.ml3
-rw-r--r--pretyping/typeclasses.ml12
-rw-r--r--pretyping/typeclasses.mli4
-rw-r--r--pretyping/unification.ml17
-rw-r--r--pretyping/unification.mli9
-rw-r--r--proofs/clenvtac.ml1
-rw-r--r--tactics/auto.ml11
-rw-r--r--tactics/auto.mli2
-rw-r--r--tactics/class_tactics.ml4172
-rw-r--r--tactics/equality.ml1
-rw-r--r--tactics/rewrite.ml4143
-rw-r--r--tactics/tactics.ml3
-rw-r--r--theories/Classes/RelationPairs.v6
-rw-r--r--theories/FSets/FMapPositive.v6
-rw-r--r--theories/FSets/FSetCompat.v2
-rw-r--r--theories/MSets/MSetInterface.v2
-rw-r--r--theories/MSets/MSetWeakList.v2
-rw-r--r--theories/Numbers/Rational/SpecViaQ/QSig.v4
-rw-r--r--theories/Structures/EqualitiesFacts.v8
-rw-r--r--theories/Structures/OrdersFacts.v2
-rw-r--r--theories/Structures/OrdersLists.v6
-rw-r--r--toplevel/classes.ml41
-rw-r--r--toplevel/classes.mli4
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacexpr.ml2
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