- 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

1 files changed, 31 insertions, 27 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index b18034b50c..c629c6c721 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