- Préservation des appels récursifs de tête dans ltac (réponse au "wish"

  implicite du rapport de bug #468); utilisation pour cela d'un
  mécanisme différent de localisation des échecs Ltac (mécanisme
  probablement à affiner). 
- Factorisation au passage des appels au débuggeur Ltac.
- Trivialités en passant dans clenv.ml.
- Tentative de documentation de l'infâme Reductionops.instance et essai 
  de déplacement plus amont du test "s = []".



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

1 files changed, 37 insertions, 5 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f247f47b66..617bd77174 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -675,10 +675,42 @@ let plain_instance s c =
   in 
   if s = [] then c else irec c
 
-(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
-let instance s c = 
-  if s = [] then c else local_strong whd_betaiota (plain_instance s c)
-
+(* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
+   has (unfortunately) different subtle side effects: 
+
+   - ** Order of subgoals **
+     If the lemma is a case analysis with parameters, it will move the
+     parameters as first subgoals (e.g. "case H" applied on
+     "H:D->A/\B|-C" will present the subgoal |-D first while w/o
+     betaiota the subgoal |-D would have come last).
+
+   - ** Betaiota-contraction in statement **
+     If the lemma has a parameter which is a function and this
+     function is applied in the lemma, then the _strong_ betaiota will
+     contract the application of the function to its argument (e.g.
+     "apply (H (fun x => x))" in "H:forall f, f 0 = 0 |- 0=0" will
+     result in applying the lemma 0=0 in which "(fun x => x) 0" has
+     been contracted). A goal to rewrite may then fail or succeed
+     differently.
+
+   - ** Naming of hypotheses ** 
+     If a lemma is a function of the form "fun H:(forall a:A, P a)
+     => .. F H .." where the expected type of H is "forall b:A, P b",
+     then, without reduction, the application of the lemma will
+     generate a subgoal "forall a:A, P a" (and intro will use name
+     "a"), while with reduction, it will generate a subgoal "forall
+     b:A, P b" (and intro will use name "b").
+
+   - ** First-order pattern-matching **
+     If a lemma has the type "(fun x => p) t" then rewriting t may fail
+     if the type of the lemma is first beta-reduced (this typically happens
+     when rewriting a single variable and the type of the lemma is obtained
+     by meta_instance (with empty map) which itself call instance with this
+     empty map.
+ *)
+
+let instance s c =
+  (* if s = [] then c else *) local_strong whd_betaiota (plain_instance s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -876,7 +908,7 @@ let meta_instance env b =
     List.map 
       (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
   in 
-  instance c_sigma b.rebus
+  if c_sigma = [] then b.rebus else instance c_sigma b.rebus
 
 let nf_meta env c = meta_instance env (mk_freelisted c)