aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/closure.ml3
-rw-r--r--checker/closure.mli3
-rw-r--r--kernel/closure.ml3
-rw-r--r--kernel/closure.mli3
-rw-r--r--pretyping/evarconv.ml181
-rw-r--r--pretyping/evarconv.mli15
-rw-r--r--pretyping/evd.ml191
-rw-r--r--pretyping/evd.mli7
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/unification.ml8
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--tactics/auto.ml3
-rw-r--r--tactics/class_tactics.ml442
-rw-r--r--tactics/rewrite.ml413
-rw-r--r--theories/FSets/FMapAVL.v5
-rw-r--r--theories/FSets/FMapInterface.v1
-rw-r--r--theories/FSets/FSetInterface.v1
-rw-r--r--theories/MSets/MSetAVL.v1
-rw-r--r--theories/Numbers/Natural/Abstract/NPow.v2
19 files changed, 202 insertions, 286 deletions
diff --git a/checker/closure.ml b/checker/closure.ml
index 8cf8c4c07..bd7347134 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -52,6 +52,9 @@ type transparent_state = Idpred.t * Cpred.t
let all_opaque = (Idpred.empty, Cpred.empty)
let all_transparent = (Idpred.full, Cpred.full)
+let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+
module type RedFlagsSig = sig
type reds
type red_kind
diff --git a/checker/closure.mli b/checker/closure.mli
index a1a23c6cb..8556f26af 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -30,6 +30,9 @@ type transparent_state = Idpred.t * Cpred.t
val all_opaque : transparent_state
val all_transparent : transparent_state
+val is_transparent_variable : transparent_state -> variable -> bool
+val is_transparent_constant : transparent_state -> constant -> bool
+
(* Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6434e1415..8d4758cfd 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -66,6 +66,9 @@ let with_stats c =
let all_opaque = (Idpred.empty, Cpred.empty)
let all_transparent = (Idpred.full, Cpred.full)
+let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+
module type RedFlagsSig = sig
type reds
type red_kind
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 74c91650a..f4dc5db35 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -29,6 +29,9 @@ val with_stats: 'a Lazy.t -> 'a
val all_opaque : transparent_state
val all_transparent : transparent_state
+val is_transparent_variable : transparent_state -> variable -> bool
+val is_transparent_constant : transparent_state -> constant -> bool
+
(** Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index df0fc161a..84b6c7b94 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -25,11 +25,11 @@ type flex_kind_of_term =
| MaybeFlexible of constr
| Flexible of existential
-let flex_kind_of_term c l =
+let flex_kind_of_term ts c l =
match kind_of_term c with
- | Const _ -> MaybeFlexible c
+ | Const n when is_transparent_constant ts n -> MaybeFlexible c
| Rel n -> MaybeFlexible c
- | Var id -> MaybeFlexible c
+ | Var id when is_transparent_variable ts id -> MaybeFlexible c
| Lambda _ when l<>[] -> MaybeFlexible c
| LetIn _ -> MaybeFlexible c
| Evar ev -> Flexible ev
@@ -157,16 +157,15 @@ let ise_array2 evd f v1 v2 =
if lv1 = Array.length v2 then allrec evd (pred lv1)
else (evd,false)
-let rec evar_conv_x env evd pbty term1 term2 =
- let sigma = evd in
- let term1 = whd_head_evar sigma term1 in
- let term2 = whd_head_evar sigma term2 in
+let rec evar_conv_x ts env evd pbty term1 term2 =
+ let term1 = whd_head_evar evd term1 in
+ let term2 = whd_head_evar evd term2 in
(* Maybe convertible but since reducing can erase evars which [evar_apprec]
could have found, we do it only if the terms are free of evar.
Note: incomplete heuristic... *)
let ground_test =
if is_ground_term evd term1 && is_ground_term evd term2 then
- if is_fconv pbty env evd term1 term2 then
+ if is_trans_fconv pbty ts env evd term1 term2 then
Some true
else if is_ground_env evd env then Some false
else None
@@ -179,40 +178,40 @@ let rec evar_conv_x env evd pbty term1 term2 =
let term1 = apprec_nohdbeta env evd term1 in
let term2 = apprec_nohdbeta env evd term2 in
if is_undefined_evar evd term1 then
- solve_simple_eqn evar_conv_x env evd
+ solve_simple_eqn (evar_conv_x ts) env evd
(position_problem true pbty,destEvar term1,term2)
else if is_undefined_evar evd term2 then
- solve_simple_eqn evar_conv_x env evd
+ solve_simple_eqn (evar_conv_x ts) env evd
(position_problem false pbty,destEvar term2,term1)
else
- evar_eqappr_x env evd pbty
+ evar_eqappr_x ts env evd pbty
(decompose_app term1) (decompose_app term2)
-and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
+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
+ match (flex_kind_of_term ts term1 l1, flex_kind_of_term ts term2 l2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
let f1 i =
if List.length l1 > List.length l2 then
let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
ise_and i
- [(fun i -> solve_simple_eqn evar_conv_x env i
+ [(fun i -> solve_simple_eqn (evar_conv_x ts) env i
(position_problem false pbty,ev2,applist(term1,deb1)));
(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) rest1 l2)]
+ (fun i -> evar_conv_x ts env i CONV) rest1 l2)]
else
let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
ise_and i
- [(fun i -> solve_simple_eqn evar_conv_x env i
+ [(fun i -> solve_simple_eqn (evar_conv_x ts) env i
(position_problem true pbty,ev1,applist(term2,deb2)));
(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) l1 rest2)]
+ (fun i -> evar_conv_x ts env i CONV) l1 rest2)]
and f2 i =
if sp1 = sp2 then
ise_and i
[(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) l1 l2);
- (fun i -> solve_refl evar_conv_x env i sp1 al1 al2,
+ (fun i -> evar_conv_x ts env i CONV) l1 l2);
+ (fun i -> solve_refl (evar_conv_x ts) env i sp1 al1 al2,
true)]
else (i,false)
in
@@ -228,7 +227,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t2 = nf_evar evd (applist appr2) in
let t2 = solve_pattern_eqn env l1 t2 in
- solve_simple_eqn evar_conv_x env evd
+ solve_simple_eqn (evar_conv_x ts) env evd
(position_problem true pbty,ev1,t2)
else if
List.length l1 <= List.length l2
@@ -240,13 +239,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
ise_and i
(* First compare extra args for better failure message *)
[(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) l1 rest2);
- (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))]
+ (fun i -> evar_conv_x ts env i CONV) l1 rest2);
+ (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
else (i,false)
and f2 i =
match eval_flexible_term env flex2 with
| Some v2 ->
- evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+ evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None -> (i,false)
in
ise_try evd [f1; f2]
@@ -261,7 +260,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t1 = nf_evar evd (applist appr1) in
let t1 = solve_pattern_eqn env l2 t1 in
- solve_simple_eqn evar_conv_x env evd
+ solve_simple_eqn (evar_conv_x ts) env evd
(position_problem false pbty,ev2,t1)
else if
List.length l2 <= List.length l1
@@ -272,13 +271,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
ise_and i
(* First compare extra args for better failure message *)
[(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) rest1 l2);
- (fun i -> evar_conv_x env i pbty (applist(term1,deb1)) term2)]
+ (fun i -> evar_conv_x ts env i CONV) rest1 l2);
+ (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
else (i,false)
and f2 i =
match eval_flexible_term env flex1 with
| Some v1 ->
- evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None -> (i,false)
in
ise_try evd [f1; f2]
@@ -286,11 +285,11 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| MaybeFlexible flex1, MaybeFlexible flex2 ->
let f1 i =
if flex1 = flex2 then
- ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
+ ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2
else
(i,false)
and f2 i =
- (try conv_record env i
+ (try conv_record ts env i
(try check_conv_record appr1 appr2
with Not_found -> check_conv_record appr2 appr1)
with Not_found -> (i,false))
@@ -303,20 +302,20 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
then
match eval_flexible_term env flex1 with
| Some v1 ->
- evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None ->
match eval_flexible_term env flex2 with
| Some v2 ->
- evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+ evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None -> (i,false)
else
match eval_flexible_term env flex2 with
| Some v2 ->
- evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+ evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None ->
match eval_flexible_term env flex1 with
| Some v1 ->
- evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None -> (i,false)
in
ise_try evd [f1; f2; f3]
@@ -329,7 +328,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
let env' = push_rel (na,None,c) env in
let appr1 = evar_apprec env' evd [] c'1 in
let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
- evar_eqappr_x env' evd CONV appr1 appr2
+ evar_eqappr_x ts env' evd CONV appr1 appr2
| (Flexible _ | MaybeFlexible _), Rigid c2 when isLambda c2 ->
assert (l2 = []);
@@ -338,7 +337,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
let env' = push_rel (na,None,c) env in
let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
let appr2 = evar_apprec env' evd [] c'2 in
- evar_eqappr_x env' evd CONV appr1 appr2
+ evar_eqappr_x ts env' evd CONV appr1 appr2
| Flexible ev1, Rigid _ ->
if
@@ -349,7 +348,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t2 = nf_evar evd (applist appr2) in
let t2 = solve_pattern_eqn env l1 t2 in
- solve_simple_eqn evar_conv_x env evd
+ solve_simple_eqn (evar_conv_x ts) env evd
(position_problem true pbty,ev1,t2)
else
(* Postpone the use of an heuristic *)
@@ -365,7 +364,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t1 = nf_evar evd (applist appr1) in
let t1 = solve_pattern_eqn env l2 t1 in
- solve_simple_eqn evar_conv_x env evd
+ solve_simple_eqn (evar_conv_x ts) env evd
(position_problem false pbty,ev2,t1)
else
(* Postpone the use of an heuristic *)
@@ -374,116 +373,116 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| MaybeFlexible flex1, Rigid _ ->
let f3 i =
- (try conv_record env i (check_conv_record appr1 appr2)
+ (try conv_record ts env i (check_conv_record appr1 appr2)
with Not_found -> (i,false))
and f4 i =
match eval_flexible_term env flex1 with
| Some v1 ->
- evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None -> (i,false)
in
ise_try evd [f3; f4]
| Rigid _ , MaybeFlexible flex2 ->
let f3 i =
- (try conv_record env i (check_conv_record appr2 appr1)
+ (try conv_record ts env i (check_conv_record appr2 appr1)
with Not_found -> (i,false))
and f4 i =
match eval_flexible_term env flex2 with
| Some v2 ->
- evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+ evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None -> (i,false)
in
ise_try evd [f3; f4]
| Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
- | Cast (c1,_,_), _ -> evar_eqappr_x env evd pbty (c1,l1) appr2
+ | Cast (c1,_,_), _ -> evar_eqappr_x ts env evd pbty (c1,l1) appr2
- | _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
+ | _, Cast (c2,_,_) -> evar_eqappr_x ts env evd pbty appr1 (c2,l2)
| Sort s1, Sort s2 when l1=[] & l2=[] ->
- (evd,base_sort_cmp pbty s1 s2)
+ (evd, base_sort_cmp pbty s1 s2)
| Lambda (na,c1,c'1), Lambda (_,c2,c'2) ->
assert (l1=[] & l2=[]);
ise_and evd
- [(fun i -> evar_conv_x env i CONV c1 c2);
+ [(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
- evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
+ evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
let f1 i =
ise_and i
- [(fun i -> evar_conv_x env i CONV b1 b2);
+ [(fun i -> evar_conv_x ts env i CONV b1 b2);
(fun i ->
let b = nf_evar i b1 in
let t = nf_evar i t1 in
- evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
+ evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) l1 l2)]
+ (fun i -> evar_conv_x ts env i CONV) l1 l2)]
and f2 i =
let appr1 = evar_apprec env i l1 (subst1 b1 c'1)
and appr2 = evar_apprec env i l2 (subst1 b2 c'2)
- in evar_eqappr_x env i pbty appr1 appr2
+ in evar_eqappr_x ts env i pbty appr1 appr2
in
ise_try evd [f1; f2]
| LetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
let appr1 = evar_apprec env evd l1 (subst1 b1 c'1)
- in evar_eqappr_x env evd pbty appr1 appr2
+ in evar_eqappr_x ts env evd pbty appr1 appr2
| _, LetIn (_,b2,_,c'2) ->
let appr2 = evar_apprec env evd l2 (subst1 b2 c'2)
- in evar_eqappr_x env evd pbty appr1 appr2
+ in evar_eqappr_x ts env evd pbty appr1 appr2
| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
ise_and evd
- [(fun i -> evar_conv_x env i CONV c1 c2);
+ [(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
- evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
+ evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
| Ind sp1, Ind sp2 ->
if eq_ind sp1 sp2 then
- ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+ ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
else (evd, false)
| Construct sp1, Construct sp2 ->
if eq_constructor sp1 sp2 then
- ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+ ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
else (evd, false)
| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
ise_and evd
- [(fun i -> evar_conv_x env i CONV p1 p2);
- (fun i -> evar_conv_x env i CONV c1 c2);
+ [(fun i -> evar_conv_x ts env i CONV p1 p2);
+ (fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i -> ise_array2 i
- (fun i -> evar_conv_x env i CONV) cl1 cl2);
- (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)]
+ (fun i -> evar_conv_x ts env i CONV) cl1 cl2);
+ (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)]
| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
if li1=li2 then
ise_and evd
[(fun i -> ise_array2 i
- (fun i -> evar_conv_x env i CONV) tys1 tys2);
+ (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
(fun i -> ise_array2 i
- (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+ (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
bds1 bds2);
(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) l1 l2)]
+ (fun i -> evar_conv_x ts env i CONV) l1 l2)]
else (evd,false)
| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
if i1=i2 then
ise_and evd
[(fun i -> ise_array2 i
- (fun i -> evar_conv_x env i CONV) tys1 tys2);
+ (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
(fun i -> ise_array2 i
- (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+ (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
bds1 bds2);
(fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) l1 l2)]
+ (fun i -> evar_conv_x ts env i CONV) l1 l2)]
else (evd,false)
(* Eta-expansion *)
@@ -493,7 +492,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
let env' = push_rel (na,None,c) env in
let appr1 = evar_apprec env' evd [] c'1 in
let appr2 = (lift 1 c2, List.map (lift 1) l2 @ [mkRel 1]) in
- evar_eqappr_x env' evd CONV appr1 appr2
+ evar_eqappr_x ts env' evd CONV appr1 appr2
| _, Lambda (na,c2,c'2) ->
assert (l2 = []);
@@ -501,7 +500,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
let env' = push_rel (na,None,c) env in
let appr1 = (lift 1 c1, List.map (lift 1) l1 @ [mkRel 1]) in
let appr2 = evar_apprec env' evd [] c'2 in
- evar_eqappr_x env' evd CONV appr1 appr2
+ evar_eqappr_x ts env' evd CONV appr1 appr2
| (Meta _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
| _, (Meta _ | Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
@@ -512,7 +511,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
-and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
let (evd',ks,_) =
List.fold_left
(fun (i,ks,m) b ->
@@ -525,29 +524,29 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
ise_and evd'
[(fun i ->
ise_list2 i
- (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x))
+ (fun i x1 x -> evar_conv_x trs env i CONV x1 (substl ks x))
params1 params);
(fun i ->
ise_list2 i
- (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
+ (fun i u1 u -> evar_conv_x trs env i CONV u1 (substl ks u))
us2 us);
- (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))));
- (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1)]
+ (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))));
+ (fun i -> ise_list2 i (fun i -> evar_conv_x trs env i CONV) ts ts1)]
(* We assume here |l1| <= |l2| *)
-let first_order_unification env evd (ev1,l1) (term2,l2) =
+let first_order_unification ts env evd (ev1,l1) (term2,l2) =
let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
ise_and evd
(* First compare extra args for better failure message *)
- [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
+ [(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
(fun i ->
(* Then instantiate evar unless already done by unifying args *)
let t2 = applist(term2,deb2) in
if is_defined_evar i ev1 then
- evar_conv_x env i CONV t2 (mkEvar ev1)
+ evar_conv_x ts env i CONV t2 (mkEvar ev1)
else
- solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))]
+ solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))]
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find_undefined evd evk in
@@ -556,7 +555,7 @@ let choose_less_dependent_instance evk evd term args =
if subst' = [] then error "Too complex unification problem." else
Evd.define evk (mkVar (fst (List.hd subst'))) evd
-let apply_conversion_problem_heuristic env evd pbty t1 t2 =
+let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let t1 = apprec_nohdbeta env evd (whd_head_evar evd t1) in
let t2 = apprec_nohdbeta env evd (whd_head_evar evd t2) in
let (term1,l1 as appr1) = decompose_app t1 in
@@ -574,19 +573,19 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
choose_less_dependent_instance evk2 evd term1 args2, true
| Evar ev1,_ when List.length l1 <= List.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
- first_order_unification env evd (ev1,l1) appr2
+ first_order_unification ts env evd (ev1,l1) appr2
| _,Evar ev2 when List.length l2 <= List.length l1 ->
(* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
- first_order_unification env evd (ev2,l2) appr1
+ first_order_unification ts env evd (ev2,l2) appr1
| _ ->
(* Some head evar have been instantiated, or unknown kind of problem *)
- evar_conv_x env evd pbty t1 t2
+ evar_conv_x ts env evd pbty t1 t2
-let consider_remaining_unif_problems env evd =
+let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
let (evd,pbs) = extract_all_conv_pbs evd in
let heuristic_solved_evd = List.fold_left
(fun evd (pbty,env,t1,t2) ->
- let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in
+ let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
evd pbs in
Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
@@ -596,22 +595,22 @@ let consider_remaining_unif_problems env evd =
(* Main entry points *)
-let the_conv_x env t1 t2 evd =
- match evar_conv_x env evd CONV t1 t2 with
+let the_conv_x ?(ts=full_transparent_state) env t1 t2 evd =
+ match evar_conv_x ts env evd CONV t1 t2 with
(evd',true) -> evd'
| _ -> raise Reduction.NotConvertible
-let the_conv_x_leq env t1 t2 evd =
- match evar_conv_x env evd CUMUL t1 t2 with
+let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd =
+ match evar_conv_x ts env evd CUMUL t1 t2 with
(evd', true) -> evd'
| _ -> raise Reduction.NotConvertible
-let e_conv env evd t1 t2 =
- match evar_conv_x env !evd CONV t1 t2 with
+let e_conv ?(ts=full_transparent_state) env evd t1 t2 =
+ match evar_conv_x ts env !evd CONV t1 t2 with
(evd',true) -> evd := evd'; true
| _ -> false
-let e_cumul env evd t1 t2 =
- match evar_conv_x env !evd CUMUL t1 t2 with
+let e_cumul ?(ts=full_transparent_state) env evd t1 t2 =
+ match evar_conv_x ts env !evd CUMUL t1 t2 with
(evd',true) -> evd := evd'; true
| _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 18a74ff5c..e1f507b0a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Names
open Term
open Sign
open Environ
@@ -13,25 +14,25 @@ open Reductionops
open Evd
(** returns exception Reduction.NotConvertible if not unifiable *)
-val the_conv_x : env -> constr -> constr -> evar_map -> evar_map
-val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map
+val the_conv_x : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
+val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
(** The same function resolving evars by side-effect and
catching the exception *)
-val e_conv : env -> evar_map ref -> constr -> constr -> bool
-val e_cumul : env -> evar_map ref -> constr -> constr -> bool
+val e_conv : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool
+val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool
(**/**)
(* For debugging *)
-val evar_conv_x :
+val evar_conv_x : transparent_state ->
env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
-val evar_eqappr_x :
+val evar_eqappr_x : transparent_state ->
env -> evar_map ->
conv_pb -> constr * constr list -> constr * constr list ->
evar_map * bool
(**/**)
-val consider_remaining_unif_problems : env -> evar_map -> evar_map
+val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
val check_conv_record : constr * types list -> constr * types list ->
constr * constr list * (constr list * constr list) *
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 3b96a4a3b..36abd5406 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -209,139 +209,9 @@ module EvarInfoMap = struct
end
-(*******************************************************************)
-(* Constraints for sort variables *)
-(*******************************************************************)
-
-type sort_var = Univ.universe
-
-type sort_constraint =
- | DefinedSort of sorts (* instantiated sort var *)
- | SortVar of sort_var list * sort_var list (* (leq,geq) *)
- | EqSort of sort_var
-
-module UniverseMap =
- Map.Make (struct type t = Univ.universe let compare = compare end)
-
-type sort_constraints = sort_constraint UniverseMap.t
-
-let rec canonical_find u scstr =
- match UniverseMap.find u scstr with
- EqSort u' -> canonical_find u' scstr
- | c -> (u,c)
-
-let whd_sort_var scstr t =
- match kind_of_term t with
- Sort(Type u) ->
- (try
- match canonical_find u scstr with
- _, DefinedSort s -> mkSort s
- | _ -> t
- with Not_found -> t)
- | _ -> t
-
-let rec set_impredicative u s scstr =
- match UniverseMap.find u scstr with
- | DefinedSort s' ->
- if family_of_sort s = family_of_sort s' then scstr
- else failwith "sort constraint inconsistency"
- | EqSort u' ->
- UniverseMap.add u (DefinedSort s) (set_impredicative u' s scstr)
- | SortVar(_,ul) ->
- (* also set sorts lower than u as impredicative *)
- UniverseMap.add u (DefinedSort s)
- (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul)
-
-let rec set_predicative u s scstr =
- match UniverseMap.find u scstr with
- | DefinedSort s' ->
- if family_of_sort s = family_of_sort s' then scstr
- else failwith "sort constraint inconsistency"
- | EqSort u' ->
- UniverseMap.add u (DefinedSort s) (set_predicative u' s scstr)
- | SortVar(ul,_) ->
- UniverseMap.add u (DefinedSort s)
- (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul)
-
-let var_of_sort = function
- Type u -> u
- | _ -> assert false
-
-let is_sort_var s scstr =
- match s with
- Type u ->
- (try
- match canonical_find u scstr with
- _, DefinedSort _ -> false
- | _ -> true
- with Not_found -> false)
- | _ -> false
-
-let new_sort_var cstr =
- let u = Termops.new_univ() in
- (u, UniverseMap.add u (SortVar([],[])) cstr)
-
-
-let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
- let rec search_rec (is_b, betw, not_betw) u1 =
- if List.mem u1 betw then (true, betw, not_betw)
- else if List.mem u1 not_betw then (is_b, betw, not_betw)
- else if u1 = u2 then (true, u1::betw,not_betw) else
- match UniverseMap.find u1 scstr with
- EqSort u1' -> search_rec (is_b,betw,not_betw) u1'
- | SortVar(leq,_) ->
- let (is_b',betw',not_betw') =
- List.fold_left search_rec (false,betw,not_betw) leq in
- if is_b' then (true, u1::betw', not_betw')
- else (false, betw', not_betw')
- | DefinedSort _ -> (false,betw,u1::not_betw) in
- let (is_betw,betw,_) = search_rec (false, [], []) u1 in
- if is_betw then
- UniverseMap.add u1 (SortVar(leq1@leq2,geq1@geq2))
- (List.fold_left
- (fun g u -> UniverseMap.add u (EqSort u1) g) scstr betw)
- else
- UniverseMap.add u1 (SortVar(u2::leq1,geq1))
- (UniverseMap.add u2 (SortVar(leq2, u1::geq2)) scstr)
-
-let set_leq s1 s2 scstr =
- let u1 = var_of_sort s1 in
- let u2 = var_of_sort s2 in
- let (cu1,c1) = canonical_find u1 scstr in
- let (cu2,c2) = canonical_find u2 scstr in
- if cu1=cu2 then scstr
- else
- match c1,c2 with
- (EqSort _, _ | _, EqSort _) -> assert false
- | SortVar(leq1,geq1), SortVar(leq2,geq2) ->
- set_leq_sort (cu1,(leq1,geq1)) (cu2,(leq2,geq2)) scstr
- | _, DefinedSort(Prop _ as s) -> set_impredicative u1 s scstr
- | _, DefinedSort(Type _) -> scstr
- | DefinedSort(Type _ as s), _ -> set_predicative u2 s scstr
- | DefinedSort(Prop _), _ -> scstr
-
-let set_sort_variable s1 s2 scstr =
- let u = var_of_sort s1 in
- match s2 with
- Prop _ -> set_impredicative u s2 scstr
- | Type _ -> set_predicative u s2 scstr
-
-let pr_sort_cstrs g =
- let l = UniverseMap.fold (fun u c l -> (u,c)::l) g [] in
- str "SORT CONSTRAINTS:" ++ fnl() ++
- prlist_with_sep fnl (fun (u,c) ->
- match c with
- EqSort u' -> Univ.pr_uni u ++ str" == " ++ Univ.pr_uni u'
- | DefinedSort s -> Univ.pr_uni u ++ str " := " ++ print_sort s
- | SortVar(leq,geq) ->
- str"[" ++ hov 0 (prlist_with_sep spc Univ.pr_uni geq) ++
- str"] <= "++ Univ.pr_uni u ++ brk(0,0) ++ str"<= [" ++
- hov 0 (prlist_with_sep spc Univ.pr_uni leq) ++ str"]")
- l
-
module EvarMap = struct
- type t = EvarInfoMap.t * sort_constraints
- let empty = EvarInfoMap.empty, UniverseMap.empty
+ type t = EvarInfoMap.t * Univ.universes
+ let empty = EvarInfoMap.empty, Univ.initial_universes
let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
let add_undefined (sigma,sm) k v = (EvarInfoMap.add_undefined sigma k v, sm)
let find (sigma,_) = EvarInfoMap.find sigma
@@ -364,11 +234,11 @@ module EvarMap = struct
let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) &&
(EvarInfoMap.exists_undefined sigma1
(fun k v -> assert (v.evar_body = Evar_empty);
- EvarInfoMap.is_defined sigma2 k)
- || not (UniverseMap.equal (=) sm1 sm2))
+ EvarInfoMap.is_defined sigma2 k))
let merge e e' = fold e' (fun n v sigma -> add sigma n v) e
-
+ let add_constraints (sigma, sm) cstrs =
+ (sigma, Univ.merge_constraints cstrs sm)
end
(*******************************************************************)
@@ -500,6 +370,8 @@ let existential_value d e = EvarMap.existential_value d.evars e
let existential_type d e = EvarMap.existential_type d.evars e
let existential_opt_value d e = EvarMap.existential_opt_value d.evars e
+let add_constraints d e = {d with evars= EvarMap.add_constraints d.evars e}
+
(*** /Lifting... ***)
(* evar_map are considered empty disregarding histories *)
@@ -519,7 +391,7 @@ let subst_evar_info s evi =
evar_body = subst_evb evi.evar_body }
let subst_evar_defs_light sub evd =
- assert (UniverseMap.is_empty (snd evd.evars));
+ assert (Univ.initial_universes = (snd evd.evars));
assert (evd.conv_pbs = []);
{ evd with
metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
@@ -617,16 +489,36 @@ let evar_list evd c =
(* Sort variables *)
let new_sort_variable ({ evars = (sigma,sm) } as d)=
- let (u,scstr) = new_sort_var sm in
- (Type u,{ d with evars = (sigma,scstr) } )
-let is_sort_variable {evars=(_,sm)} s =
- is_sort_var s sm
-let whd_sort_variable {evars=(_,sm)} t = whd_sort_var sm t
-let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
- { d with evars = (sigma, set_leq u1 u2 sm) }
-let define_sort_variable ({evars=(sigma,sm)}as d) u s =
- { d with evars = (sigma, set_sort_variable u s sm) }
-let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
+ let u = Termops.new_univ() in
+ (Type u, d)
+
+let is_sort_variable {evars=(_,sm)} s = match s with Type _ -> true | _ -> false
+let whd_sort_variable {evars=(_,sm)} t = t
+
+let univ_of_sort = function
+ | Type u -> u
+ | Prop Pos -> Univ.type0_univ
+ | Prop Null -> Univ.type0m_univ
+
+let set_leq_sort d s1 s2 =
+ if s1 = s2 then d
+ else
+ let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in
+ match s1, s2 with
+ | Prop c, Prop c' ->
+ if c = Null && c' = Pos then d
+ else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)))
+ | _, _ ->
+ add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint)
+
+let set_eq_sort d s1 s2 =
+ if s1 = s2 then d
+ else
+ let u1, u2 = univ_of_sort s1, univ_of_sort s2 in
+ match s1, s2 with
+ | Prop c, Prop c' -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2))
+ | _, _ ->
+ add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
(**********************************************************)
(* Accessing metas *)
@@ -823,7 +715,7 @@ let pr_evar_info evi =
in
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
-let pr_evar_map_t (evars,cstrs as sigma) =
+let pr_evar_map_t (evars,univs as sigma) =
let evs =
if evars = EvarInfoMap.empty then mt ()
else
@@ -833,8 +725,9 @@ let pr_evar_map_t (evars,cstrs as sigma) =
h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
(EvarMap.to_list sigma))++fnl()
and cs =
- if cstrs = UniverseMap.empty then mt ()
- else pr_sort_cstrs cstrs++fnl()
+ if univs = Univ.initial_universes then mt ()
+ else str"UNIVERSES:"++brk(0,1)++
+ h 0 (Univ.pr_universes univs)++fnl()
in evs ++ cs
let pr_constraints pbs =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 751009434..8c31d6af3 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -162,6 +162,8 @@ val is_evar : evar_map -> evar -> bool
val is_defined : evar_map -> evar -> bool
val is_undefined : evar_map -> evar -> bool
+val add_constraints : evar_map -> Univ.constraints -> evar_map
+
(** {6 ... } *)
(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
no body and [Not_found] if it does not exist in [sigma] *)
@@ -248,8 +250,8 @@ val subst_defined_metas : metabinding list -> constr -> constr option
val new_sort_variable : evar_map -> sorts * evar_map
val is_sort_variable : evar_map -> sorts -> bool
val whd_sort_variable : evar_map -> constr -> constr
-val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map
-val define_sort_variable : evar_map -> sorts -> sorts -> evar_map
+val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
+val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
(********************************************************************
constr with holes *)
@@ -275,7 +277,6 @@ type unsolvability_explanation = SeveralInstancesFound of int
val pr_evar_info : evar_info -> Pp.std_ppcmds
val pr_evar_map : evar_map -> Pp.std_ppcmds
-val pr_sort_constraints : evar_map -> Pp.std_ppcmds
val pr_metaset : Metaset.t -> Pp.std_ppcmds
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 689e544b8..92ad6bea6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -605,8 +605,8 @@ let is_conv env sigma = test_conversion Reduction.conv env sigma
let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
-let test_trans_conversion f reds env sigma x y =
- try let _ = f reds env (nf_evar sigma x) (nf_evar sigma y) in true
+let test_trans_conversion (f:?evars:'a->'b) reds env sigma x y =
+ try let _ = f ~evars:(safe_evar_value sigma) reds env x y in true
with NotConvertible -> false
| Anomaly _ -> error "Conversion test raised an anomaly"
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fd287f3af..6121ba7d8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -637,8 +637,8 @@ let order_metas metas =
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
-let solve_simple_evar_eqn env evd ev rhs =
- let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
+let solve_simple_evar_eqn ts env evd ev rhs =
+ let evd,b = solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) in
if not b then error_cannot_unify env evd (mkEvar ev,rhs);
Evarconv.consider_remaining_unif_problems env evd
@@ -669,12 +669,12 @@ let w_merge env with_types flags (evd,metas,evars) =
w_merge_rec evd' metas evars eqns
else
let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
- w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
+ w_merge_rec (solve_simple_evar_eqn flags.modulo_delta env evd' ev rhs'')
metas evars' eqns
| _ ->
let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
- w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
+ w_merge_rec (solve_simple_evar_eqn flags.modulo_delta env evd' ev rhs'')
metas evars' eqns
end
| [] ->
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fdd510831..36268de1e 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -30,7 +30,7 @@ let define_and_solve_constraints evk c evd =
let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
fst (List.fold_left
(fun (evd,b as p) (pbty,env,t1,t2) ->
- if b then Evarconv.evar_conv_x env evd pbty t1 t2 else p) (evd,true)
+ if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true)
pbs)
with e when Pretype_errors.precatchable_exception e ->
error "Instance does not satisfy constraints."
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f4985f40e..d03c527f4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -880,9 +880,10 @@ let add_hint_lemmas eapply lems hint_db gl =
let make_local_hint_db eapply lems gl =
let sign = pf_hyps gl in
+ let ts = Hint_db.transparent_state (searchtable_map "core") in
let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in
add_hint_lemmas eapply lems
- (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false)) gl
+ (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl
(* Serait-ce possible de compiler d'abord la tactique puis de faire la
substitution sans passer par bdize dont l'objectif est de préparer un
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5553f6035..3551b75e5 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -307,24 +307,24 @@ let hints_tac hints =
in
let tacs = List.sort compare tacs in
let rec aux i = function
- | (_, pp, b, {it = gls; sigma = s}) :: tl ->
+ | (_, 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 =
+ 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
+ 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
+ | None -> gls', s'
| Some (evgls, s') ->
(gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s')
in
@@ -333,7 +333,7 @@ let hints_tac hints =
{ 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
+ 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 }
@@ -443,19 +443,6 @@ let resolve_all_evars_once debug (mode, depth) p evd =
let db = searchtable_map typeclasses_db in
real_eauto (Hint_db.transparent_state db) [db] p evd
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
- let (gl,t,sigma) =
- Goal.V82.mk_goal sigma (Environ.named_context_val env) gl Store.empty in
- let gls = { it = gl ; sigma = sigma } in
- let hints = searchtable_map typeclasses_db in
- let gls' = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in
- let evd = sig_sig gls' in
- let term = Evarutil.nf_evar evd t in
- evd, term
-
-let _ =
- Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
-
(** We compute dependencies via a union-find algorithm.
Beware of the imperative effects on the partition structure,
it should not be shared, but only used locally. *)
@@ -476,6 +463,19 @@ let evar_dependencies evm p =
in Intpart.union_set evars p)
evm ()
+let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
+ let (gl,t,sigma) =
+ Goal.V82.mk_goal sigma (Environ.named_context_val env) gl Store.empty in
+ let gls = { it = gl ; sigma = sigma } in
+ let hints = searchtable_map typeclasses_db in
+ let gls' = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in
+ let evd = sig_sig gls' in
+ let term = Evarutil.nf_evar evd t in
+ evd, term
+
+let _ =
+ Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
+
(** [split_evars] returns groups of undefined evars according to dependencies *)
let split_evars evm =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 127a61db5..737b55750 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1029,7 +1029,9 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
| Some id -> pf_get_hyp_typ gl id, Some id
| None -> pf_concl gl, None
in
- let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] (project gl) concl is_hyp in
+ let sigma = project gl in
+ let concl = Evarutil.nf_evar sigma concl in
+ let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
treat res
with
| Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
@@ -1683,7 +1685,10 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
let get_hyp gl evars (c,l) clause l2r =
let hi = decompose_applied_relation (pf_env gl) evars None (c,l) l2r in
- let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl 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
let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
@@ -1702,8 +1707,8 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
try
tclWEAK_PROGRESS
(tclTHEN
- (Refiner.tclEVARS hypinfo.cl.evd)
- (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl
+ (Refiner.tclEVARS hypinfo.cl.evd)
+ (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl
with RewriteFailure ->
let {l2r=l2r; c1=x; c2=y} = hypinfo in
raise (Pretype_errors.PretypeError
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 516015ab9..5a9b5d898 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -37,6 +37,7 @@ Open Local Scope lazy_bool_scope.
Open Local Scope Int_scope.
Definition key := X.t.
+Hint Transparent key.
(** * Trees *)
@@ -821,7 +822,7 @@ Proof.
intros l x e r; functional induction (bal l x e r); intros; clearf;
inv bst; repeat apply create_bst; auto; unfold create; try constructor;
(apply lt_tree_node || apply gt_tree_node); auto;
- (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
+ (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
Qed.
Hint Resolve bal_bst.
@@ -1331,7 +1332,7 @@ Proof.
inversion_clear H.
destruct H7; simpl in *.
order.
- destruct (elements_aux_mapsto r acc x e0); intuition eauto.
+ destruct (elements_aux_mapsto r acc x e0); intuition eauto.
Qed.
Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s).
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 252e67930..4d89b562d 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -56,6 +56,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
Module Type WSfun (E : DecidableType).
Definition key := E.t.
+ Hint Transparent key.
Parameter t : Type -> Type.
(** the abstract type of maps *)
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index a23263890..a03611193 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -251,6 +251,7 @@ Module Type WSfun (E : DecidableType).
End Spec.
+ Hint Transparent elt.
Hint Resolve mem_1 equal_1 subset_1 empty_1
is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
remove_2 singleton_2 union_1 union_2 union_3
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 253267fc8..5d17dd3f1 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -46,6 +46,7 @@ Local Open Scope Int_scope.
Local Open Scope lazy_bool_scope.
Definition elt := X.t.
+Hint Transparent elt.
(** ** Trees
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index 67ed77981..b046e383d 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -96,7 +96,7 @@ Definition pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
(** Injectivity *)
Lemma pow_inj_l : forall a b c, c~=0 -> a^c == b^c -> a == b.
-Proof. intros; eapply pow_inj_l; eauto; auto'. auto'. Qed.
+Proof. intros; eapply pow_inj_l; eauto; auto'. Qed.
Lemma pow_inj_r : forall a b c, 1<a -> a^b == a^c -> b == c.
Proof. intros; eapply pow_inj_r; eauto; auto'. Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 22:50:43 +0000