From 9221176c38519e17522104f5adbbec3fcf755dd4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 10 Aug 2011 19:28:41 +0000 Subject: 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 --- kernel/vconv.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/vconv.ml') 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 -- cgit v1.2.3