Propagated information from the reduction tactics to the kernel so

that the kernel conversion solves the delta/delta critical pair the
same way the tactics did. This allows to improve Qed time when slow
down is due to conversion having (arbitrarily) made the wrong choice.
Propagation is done thanks to a new kind of cast called REVERTcast.

Notes:
- Vm conversion not modified
- size of vo generally grows because of additional casts
- this remains a heuristic... for the record, when a reduction tactic
  is applied on the goal t leading to new goal t', this is translated
  in the kernel in a conversion t' <= t where, hence, reducing in t'
  must be preferred; what the propagation of reduction cast to the
  kernel does not do is whether it is preferable to first unfold c or
  to first compare u' and u in "c u' = c u"; in particular,
  intermediate casts are sometimes useful to solve this kind of issues
  (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the
  combination "simpl;red" needs the intermediate cast to ensure Qed
  answers quickly); henceforth the merge of nested casts in mkCast is
  deactivated
- for tactic "change", REVERTcast should be used when conversion is in
  the hypotheses, but convert_hyp does not (yet) support this (would
  require e.g. that convert_hyp overwrite some given hyp id with a
  body-cleared let-binding new_id := Cast(old_id,REVERTCast,t))

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 95 insertions, 86 deletions

diff --git a/CHANGES b/CHANGES
index 673649ee91..8d0623f585 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 6ad4c38fc6..92109258d7 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 a41b02f0cb..09ca4b92bb 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 1a286bb16c..fc5e32cf5c 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 bee8815a25..aa78fbdad3 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 9ff8ee9ca9..b308b22a4b 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 6fb8843180..68fbd1807e 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 c9112e86dd..9173ab8cde 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 bf3640e35c..4d0edc689e 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 940e14554b..c0d031709b 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 2762a52a16..834c27969e 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 31bf431da1..4610c06ce5 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 e72580e696..3801a6fd88 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 92addc646d..b14567938e 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)