- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771

  (les let-in étaient comptés comme des produits, introduisant une incohérence
  sur le nombre de produits à instancier dans les lemmes appelés par apply).
- Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition.
- Doc développeur



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

4 files changed, 55 insertions, 31 deletions

diff --git a/CHANGES b/CHANGES
index aa8a59413..9db0cec4e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,13 +1,18 @@
-Changes from V8.1gamma to ...
-=============================
+Changes from V8.1 to V8.2
+=========================
 
 Commands
 
 - Added option Global to "Implicit Arguments" and "Arguments Scope" for
   section surviving.
-
 - Added option "Unset Elimination Schemes" to deactivated the automatic
-generation of elimination schemes.
+  generation of elimination schemes.
+
+Libraries
+
+- Better computational behavior of some constants (eq_nat_dec more
+  efficient, Z_lt_le_dec transparent, ...) [exceptionally source of
+  incompatibilities].
 
 Notations
 
@@ -31,6 +36,7 @@ Tactics
   ident], [apply <- term in ident] for applying equivalences (iff).
 - Slight improvement of the hnf and simpl tactics when applied on
   expressions with explicit occurrences of match or fix.
+- Better heuristic of lemma unfolding for apply/eapply.
 
 Changes from V8.1gamma to V8.1
 ==============================
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 90e294968..ad5704db8 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,16 @@
 =========================================
+= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
+=========================================
+
+A few differences in Coq ML interfaces between Coq V8.0 and V8.1
+================================================================
+
+** Functions
+
+Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
+
+
+=========================================
 = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
 =========================================
 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index b18034b50..c629c6c72 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -93,39 +93,43 @@ let clenv_push_prod cl =
     | _ -> raise NotExtensibleClause
   in clrec typ
 
-let clenv_environments evd bound c =
-  let rec clrec (e,metas) n c =
-    match n, kind_of_term c with
-      | (Some 0, _) -> (e, List.rev metas, c)
-      | (n, Cast (c,_,_)) -> clrec (e,metas) n c
-      | (n, Prod (na,c1,c2)) ->
+(* Instantiate the first [bound] products of [t] with metas (all products if
+   [bound] is [None]; unfold local defs *)
+
+let clenv_environments evd bound t =
+  let rec clrec (e,metas) n t =
+    match n, kind_of_term t with
+      | (Some 0, _) -> (e, List.rev metas, t)
+      | (n, Cast (t,_,_)) -> clrec (e,metas) n t
+      | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = dependent (mkRel 1) c2 in
+	  let dep = dependent (mkRel 1) t2 in
 	  let na' = if dep then na else Anonymous in
-	  let e' = meta_declare mv c1 ~name:na' e in
+	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n)
-	    (if dep then (subst1 (mkMeta mv) c2) else c2)
-      | (n, LetIn (na,b,_,c)) ->
-	  clrec (e,metas) (option_map ((+) (-1)) n) (subst1 b c)
-      | (n, _) -> (e, List.rev metas, c)
+	    (if dep then (subst1 (mkMeta mv) t2) else t2)
+      | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
+      | (n, _) -> (e, List.rev metas, t)
   in 
-  clrec (evd,[]) bound c
-
-let clenv_environments_evars env evd bound c =
-  let rec clrec (e,ts) n c =
-    match n, kind_of_term c with
-      | (Some 0, _) -> (e, List.rev ts, c)
-      | (n, Cast (c,_,_)) -> clrec (e,ts) n c
-      | (n, Prod (na,c1,c2)) ->
-          let e',constr = Evarutil.new_evar e env c1 in
-	  let dep = dependent (mkRel 1) c2 in
+  clrec (evd,[]) bound t
+
+(* Instantiate the first [bound] products of [t] with evars (all products if
+   [bound] is [None]; unfold local defs *)
+
+let clenv_environments_evars env evd bound t =
+  let rec clrec (e,ts) n t =
+    match n, kind_of_term t with
+      | (Some 0, _) -> (e, List.rev ts, t)
+      | (n, Cast (t,_,_)) -> clrec (e,ts) n t
+      | (n, Prod (na,t1,t2)) ->
+          let e',constr = Evarutil.new_evar e env t1 in
+	  let dep = dependent (mkRel 1) t2 in
 	  clrec (e', constr::ts) (option_map ((+) (-1)) n)
-	    (if dep then (subst1 constr c2) else c2)
-      | (n, LetIn (na,b,_,c)) ->
-	  clrec (e,ts) (option_map ((+) (-1)) n) (subst1 b c)
-      | (n, _) -> (e, List.rev ts, c)
+	    (if dep then (subst1 constr t2) else t2)
+      | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
+      | (n, _) -> (e, List.rev ts, t)
   in 
-  clrec (evd,[]) bound c
+  clrec (evd,[]) bound t
 
 let clenv_conv_leq env sigma t c bound =
   let ty = Retyping.get_type_of env sigma c in
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 10046a1c3..589ac5abe 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -22,6 +22,8 @@ val e_assumption : tactic
 
 val registered_e_assumption : tactic
 
+val simplest_eapply : constr -> tactic
+
 val e_give_exact_constr : constr -> tactic
 
 val gen_eauto : bool -> bool * int -> constr list ->