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
---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

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
 
-- 
cgit v1.2.3