- 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

2 files changed, 40 insertions, 7 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 2d26e5bb1..dbc51514c 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -62,6 +62,7 @@ let subst_clenv sub clenv =
     env = clenv.env }
 
 let clenv_nf_meta clenv c = nf_meta clenv.evd c
+let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
 let clenv_value clenv = meta_instance clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
@@ -313,12 +314,12 @@ let clenv_fchain ?(allow_K=true) mv clenv nextclenv =
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
     clenv_unify allow_K CUMUL
-      (clenv_nf_meta clenv' nextclenv.templtyp.rebus)
+      (clenv_term clenv' nextclenv.templtyp)
       (clenv_meta_type clenv' mv)
       clenv' in
   (* assign the metavar *)
   let clenv''' =
-    clenv_assign mv (clenv_nf_meta clenv' nextclenv.templval.rebus) clenv''
+    clenv_assign mv (clenv_term clenv' nextclenv.templval) clenv''
   in 
   clenv'''
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f247f47b6..617bd7717 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)