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

2 files changed, 3 insertions, 3 deletions

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