aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--kernel/conv_oracle.ml4
-rw-r--r--kernel/conv_oracle.mli2
-rw-r--r--kernel/reduction.ml96
-rw-r--r--kernel/reduction.mli20
-rw-r--r--kernel/term.ml4
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/typeops.ml10
-rw-r--r--kernel/vconv.ml6
-rw-r--r--parsing/ppconstr.ml2
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/logic.ml2
-rw-r--r--tactics/tactics.ml25
14 files changed, 95 insertions, 86 deletions
diff --git a/CHANGES b/CHANGES
index 673649ee9..8d0623f58 100644
--- a/CHANGES
+++ b/CHANGES
@@ -52,6 +52,8 @@ Vernacular commands
- The undocumented and obsolete option "Set/Unset Boxed Definitions" has
been removed, as well as syntaxes like "Boxed Fixpoint foo".
- A new option "Set Default Timeout n / Unset Default Timeout".
+- Qed now uses information from the reduction tactics used in proof script
+ to avoid conversion at Qed time to go into a very long computation.
Module System
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 6ad4c38fc..92109258d 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -56,12 +56,12 @@ let get_transp_state () =
(* Unfold the first constant only if it is "more transparent" than the
second one. In case of tie, expand the second one. *)
-let oracle_order k1 k2 =
+let oracle_order l2r k1 k2 =
match get_strategy k1, get_strategy k2 with
| Expand, _ -> true
| Level n1, Opaque -> true
| Level n1, Level n2 -> n1 < n2
- | _ -> false (* expand k2 *)
+ | _ -> l2r (* use recommended default *)
(* summary operations *)
let init() = (cst_opacity := Cmap.empty; var_opacity := Idmap.empty)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index a41b02f0c..09ca4b92b 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -12,7 +12,7 @@ open Names
If [oracle_order kn1 kn2] is true, then unfold kn1 first.
Note: the oracle does not introduce incompleteness, it only
tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : 'a tableKey -> 'a tableKey -> bool
+val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
(** Priority for the expansion of constant in the conversion test.
* Higher levels means that the expansion is less prioritary.
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1a286bb16..fc5e32cf5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -239,11 +239,11 @@ let in_whnf (t,stk) =
| FLOCKED -> assert false
(* Conversion between [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv =
- eqappr cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+ eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Util.check_for_interrupt ();
(* First head reduce both terms *)
let rec whd_both (t1,stk1) (t2,stk2) =
@@ -267,13 +267,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
sort_cmp cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if n=m
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| _ -> raise NotConvertible)
| (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
if ev1=ev2 then
- let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in
- convert_vect infos el1 el2
+ let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
+ convert_vect l2r infos el1 el2
(Array.map (mk_clos env1) args1)
(Array.map (mk_clos env2) args2) u1
else raise NotConvertible
@@ -281,19 +281,19 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
(* 2 index known to be bound to no constant *)
| (FRel n, FRel m) ->
if reloc_rel n el1 = reloc_rel m el2
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try (* try first intensional equality *)
if eq_table_key fl1 fl2
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
with NotConvertible ->
(* else the oracle tells which constant is to be expanded *)
let (app1,app2) =
- if Conv_oracle.oracle_order fl1 fl2 then
+ if Conv_oracle.oracle_order l2r fl1 fl2 then
match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
| None ->
@@ -307,7 +307,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
(match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
| None -> raise NotConvertible) in
- eqappr cv_pb infos app1 app2 cuniv)
+ eqappr cv_pb l2r infos app1 app2 cuniv)
(* other constructors *)
| (FLambda _, FLambda _) ->
@@ -317,40 +317,40 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
anomaly "conversion was given ill-typed terms (FLambda)";
let (_,ty1,bd1) = destFLambda mk_clos hd1 in
let (_,ty2,bd2) = destFLambda mk_clos hd2 in
- let u1 = ccnv CONV infos el1 el2 ty1 ty2 cuniv in
- ccnv CONV infos (el_lift el1) (el_lift el2) bd1 bd2 u1
+ let u1 = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
+ ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 u1
| (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly "conversion was given ill-typed terms (FProd)";
(* Luo's system *)
- let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
- ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
+ let u1 = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
+ ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 u1
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
if v1 <> [] then
anomaly "conversion was given unreduced term (FLambda)";
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
- eqappr CONV infos
+ eqappr CONV l2r infos
(el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
| (_, FLambda _) ->
if v2 <> [] then
anomaly "conversion was given unreduced term (FLambda)";
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
- eqappr CONV infos
+ eqappr CONV l2r infos
(el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
(* only one constant, defined var or defined rel *)
| (FFlex fl1, _) ->
(match unfold_reference infos fl1 with
| Some def1 ->
- eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
+ eqappr cv_pb l2r infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
| None -> raise NotConvertible)
| (_, FFlex fl2) ->
(match unfold_reference infos fl2 with
| Some def2 ->
- eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
+ eqappr cv_pb l2r infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
| None -> raise NotConvertible)
(* Inductive types: MutInd MutConstruct Fix Cofix *)
@@ -358,13 +358,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
| (FInd ind1, FInd ind2) ->
if eq_ind ind1 ind2
then
- convert_stacks infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
if j1 = j2 && eq_ind ind1 ind2
then
- convert_stacks infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
@@ -375,11 +375,11 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
- let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
+ let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let u2 =
- convert_vect infos
+ convert_vect l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
- convert_stacks infos lft1 lft2 v1 v2 u2
+ convert_stacks l2r infos lft1 lft2 v1 v2 u2
else raise NotConvertible
| (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
@@ -390,11 +390,11 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
- let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
+ let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let u2 =
- convert_vect infos
+ convert_vect l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
- convert_stacks infos lft1 lft2 v1 v2 u2
+ convert_stacks l2r infos lft1 lft2 v1 v2 u2
else raise NotConvertible
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
@@ -405,13 +405,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
(* In all other cases, terms are not convertible *)
| _ -> raise NotConvertible
-and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
compare_stacks
- (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
+ (fun (l1,t1) (l2,t2) c -> ccnv CONV l2r infos l1 l2 t1 t2 c)
(eq_ind)
lft1 stk1 lft2 stk2 cuniv
-and convert_vect infos lft1 lft2 v1 v2 cuniv =
+and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let lv1 = Array.length v1 in
let lv2 = Array.length v2 in
if lv1 = lv2
@@ -419,34 +419,34 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
let rec fold n univ =
if n >= lv1 then univ
else
- let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in
+ let u1 = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) univ in
fold (n+1) u1 in
fold 0 cuniv
else raise NotConvertible
-let clos_fconv trans cv_pb evars env t1 t2 =
+let clos_fconv trans cv_pb l2r evars env t1 t2 =
let infos = trans, create_clos_infos ~evars betaiotazeta env in
- ccnv cv_pb infos el_id el_id (inject t1) (inject t2) empty_constraint
+ ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) empty_constraint
-let trans_fconv reds cv_pb evars env t1 t2 =
+let trans_fconv reds cv_pb l2r evars env t1 t2 =
if eq_constr t1 t2 then empty_constraint
- else clos_fconv reds cv_pb evars env t1 t2
+ else clos_fconv reds cv_pb l2r evars env t1 t2
-let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None)
-let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars
-let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars
+let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->None)
+let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars
+let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars
let fconv = trans_fconv (Idpred.full, Cpred.full)
-let conv_cmp cv_pb = fconv cv_pb (fun _->None)
-let conv ?(evars=fun _->None) = fconv CONV evars
-let conv_leq ?(evars=fun _->None) = fconv CUMUL evars
+let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
+let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
+let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars
-let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
+let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
array_fold_left2_i
(fun i c t1 t2 ->
let c' =
- try conv_leq ~evars env t1 t2
+ try conv_leq ~l2r ~evars env t1 t2
with NotConvertible -> raise (NotConvertibleVect i) in
union_constraints c c')
empty_constraint
@@ -455,26 +455,26 @@ let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
(* option for conversion *)
-let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
+let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
let set_vm_conv f = vm_conv := f
let vm_conv cv_pb env t1 t2 =
try
!vm_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb (fun _->None) env t1 t2
+ fconv cv_pb false (fun _->None) env t1 t2
-let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
+let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
let set_default_conv f = default_conv := f
-let default_conv cv_pb env t1 t2 =
+let default_conv cv_pb ?(l2r=false) env t1 t2 =
try
- !default_conv cv_pb env t1 t2
+ !default_conv ~l2r cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb (fun _->None) env t1 t2
+ fconv cv_pb false (fun _->None) env t1 t2
let default_conv_leq = default_conv CUMUL
(*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index bee8815a2..aa78fbdad 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -36,27 +36,27 @@ val sort_cmp :
val conv_sort : sorts conversion_function
val conv_sort_leq : sorts conversion_function
-val trans_conv_cmp : conv_pb -> constr trans_conversion_function
+val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function
val trans_conv :
- ?evars:(existential->constr option) -> constr trans_conversion_function
+ ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function
val trans_conv_leq :
- ?evars:(existential->constr option) -> types trans_conversion_function
+ ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function
-val conv_cmp : conv_pb -> constr conversion_function
+val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function
val conv :
- ?evars:(existential->constr option) -> constr conversion_function
+ ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function
val conv_leq :
- ?evars:(existential->constr option) -> types conversion_function
+ ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function
val conv_leq_vecti :
- ?evars:(existential->constr option) -> types array conversion_function
+ ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function
(** option for conversion *)
val set_vm_conv : (conv_pb -> types conversion_function) -> unit
val vm_conv : conv_pb -> types conversion_function
-val set_default_conv : (conv_pb -> types conversion_function) -> unit
-val default_conv : conv_pb -> types conversion_function
-val default_conv_leq : types conversion_function
+val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
+val default_conv : conv_pb -> ?l2r:bool -> types conversion_function
+val default_conv_leq : ?l2r:bool -> types conversion_function
(************************************************************************)
diff --git a/kernel/term.ml b/kernel/term.ml
index 9ff8ee9ca..b308b22a4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -34,7 +34,7 @@ type existential_key = int
type metavariable = int
(* This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | DEFAULTcast
+type cast_kind = VMcast | DEFAULTcast | REVERTcast
(* This defines Cases annotations *)
type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
@@ -135,7 +135,7 @@ let mkSort = function
(* (that means t2 is declared as the type of t1) *)
let mkCast (t1,k2,t2) =
match t1 with
- | Cast (c,k1, _) when k1 = k2 -> Cast (c,k1,t2)
+ | Cast (c,k1, _) when k1 = VMcast & k1 = k2 -> Cast (c,k1,t2)
| _ -> Cast (t1,k2,t2)
(* Constructs the product (x:t1)t2 *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 6fb884318..68fbd1807 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -93,7 +93,7 @@ val mkType : Univ.universe -> types
(** This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | DEFAULTcast
+type cast_kind = VMcast | DEFAULTcast | REVERTcast
(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
type t{_ 2} (that means t2 is declared as the type of t1). *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c9112e86d..9173ab8cd 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -18,7 +18,7 @@ open Reduction
open Inductive
open Type_errors
-let conv_leq = default_conv CUMUL
+let conv_leq l2r = default_conv CUMUL ~l2r
let conv_leq_vecti env v1 v2 =
array_fold_left2_i
@@ -191,6 +191,8 @@ let judge_of_letin env name defj typj j =
(* Type of an application. *)
+let has_revert c = match kind_of_term c with Cast (c,REVERTcast,_) -> true | _ -> false
+
let judge_of_apply env funj argjv =
let rec apply_rec n typ cst = function
| [] ->
@@ -201,7 +203,8 @@ let judge_of_apply env funj argjv =
(match kind_of_term (whd_betadeltaiota env typ) with
| Prod (_,c1,c2) ->
(try
- let c = conv_leq env hj.uj_type c1 in
+ let l2r = has_revert hj.uj_val in
+ let c = conv_leq l2r env hj.uj_type c1 in
let cst' = union_constraints cst c in
apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
with NotConvertible ->
@@ -268,7 +271,8 @@ let judge_of_cast env cj k tj =
let cst =
match k with
| VMcast -> vm_conv CUMUL env cj.uj_type expected_type
- | DEFAULTcast -> conv_leq env cj.uj_type expected_type in
+ | DEFAULTcast -> conv_leq false env cj.uj_type expected_type
+ | REVERTcast -> conv_leq true env cj.uj_type expected_type in
{ uj_val = mkCast (cj.uj_val, k, expected_type);
uj_type = expected_type },
cst
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index bf3640e35..4d0edc689 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -100,7 +100,7 @@ and conv_atom pb k a1 stk1 a2 stk2 cu =
conv_stack k stk1 stk2 cu
else raise NotConvertible
with NotConvertible ->
- if oracle_order ik1 ik2 then
+ if oracle_order false ik1 ik2 then
conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
end
@@ -236,8 +236,8 @@ let use_vm = ref false
let set_use_vm b =
use_vm := b;
- if b then Reduction.set_default_conv vconv
- else Reduction.set_default_conv Reduction.conv_cmp
+ if b then Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> vconv cv_pb)
+ else Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> Reduction.conv_cmp cv_pb)
let use_vm _ = !use_vm
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 940e14554..c0d031709 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -519,7 +519,7 @@ let pr pr sep inherited a =
| CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
| CSort (_,s) -> pr_glob_sort s, latom
| CCast (_,a,CastConv (k,b)) ->
- let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in
+ let s = match k with VMcast -> "<:" | DEFAULTcast | REVERTcast -> ":" in
hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
lcast
| CCast (_,a,CastCoerce) ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2762a52a1..834c27969 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -606,7 +606,7 @@ let pb_equal = function
let sort_cmp = sort_cmp
-let test_conversion (f:?evars:'a->'b) env sigma x y =
+let test_conversion (f: ?l2r:bool-> ?evars:'a->'b) env sigma x y =
try let _ =
f ~evars:(safe_evar_value sigma) env x y in true
with NotConvertible -> false
@@ -616,7 +616,7 @@ 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:?evars:'a->'b) reds env sigma x y =
+let test_trans_conversion (f: ?l2r:bool-> ?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 31bf431da..4610c06ce 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -325,7 +325,7 @@ let oracle_order env cf1 cf2 =
| Some k1 ->
match cf2 with
| None -> Some true
- | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
+ | Some k2 -> Some (Conv_oracle.oracle_order false k1 k2)
let do_reduce ts (env, nb) sigma c =
let (t, stack') = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e72580e69..3801a6fd8 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -627,7 +627,7 @@ let prim_refiner r sigma goal =
check_typability env sigma cl';
if (not !check) || is_conv_leq env sigma cl' cl then
let (sg,ev,sigma) = mk_goal sign cl' in
- let ev = if k=VMcast then mkCast(ev,k,cl) else ev in
+ let ev = if k<>DEFAULTcast then mkCast(ev,k,cl) else ev in
let sigma = Goal.V82.partial_solution sigma goal ev in
([sg], sigma)
else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 92addc646..b14567938 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -267,9 +267,12 @@ let reduct_in_hyp redfun (id,where) gl =
convert_hyp_no_check
(pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl
+let revert_cast (redfun,kind as r) =
+ if kind = DEFAULTcast then (redfun,REVERTcast) else r
+
let reduct_option redfun = function
| Some id -> reduct_in_hyp (fst redfun) id
- | None -> reduct_in_concl redfun
+ | None -> reduct_in_concl (revert_cast redfun)
(* Now we introduce different instances of the previous tacticals *)
let change_and_check cv_pb t env sigma c =
@@ -305,21 +308,21 @@ let change chg c cls gl =
cls gl
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let try_red_in_concl = reduct_in_concl (try_red_product,DEFAULTcast)
-let red_in_concl = reduct_in_concl (red_product,DEFAULTcast)
+let try_red_in_concl = reduct_in_concl (try_red_product,REVERTcast)
+let red_in_concl = reduct_in_concl (red_product,REVERTcast)
let red_in_hyp = reduct_in_hyp red_product
-let red_option = reduct_option (red_product,DEFAULTcast)
-let hnf_in_concl = reduct_in_concl (hnf_constr,DEFAULTcast)
+let red_option = reduct_option (red_product,REVERTcast)
+let hnf_in_concl = reduct_in_concl (hnf_constr,REVERTcast)
let hnf_in_hyp = reduct_in_hyp hnf_constr
-let hnf_option = reduct_option (hnf_constr,DEFAULTcast)
-let simpl_in_concl = reduct_in_concl (simpl,DEFAULTcast)
+let hnf_option = reduct_option (hnf_constr,REVERTcast)
+let simpl_in_concl = reduct_in_concl (simpl,REVERTcast)
let simpl_in_hyp = reduct_in_hyp simpl
-let simpl_option = reduct_option (simpl,DEFAULTcast)
-let normalise_in_concl = reduct_in_concl (compute,DEFAULTcast)
+let simpl_option = reduct_option (simpl,REVERTcast)
+let normalise_in_concl = reduct_in_concl (compute,REVERTcast)
let normalise_in_hyp = reduct_in_hyp compute
-let normalise_option = reduct_option (compute,DEFAULTcast)
+let normalise_option = reduct_option (compute,REVERTcast)
let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
-let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,DEFAULTcast)
+let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast)
let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 14:46:59 +0000