Remove avoidable use of GDynamic

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

1 files changed, 7 insertions, 14 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8021d742b..c65d3181c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1109,7 +1109,11 @@ let (value_f:constr list -> global_reference -> constr) =
 	  al
       )
     in
-    let fun_body =
+    let context = List.map
+      (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al))
+    in
+    let env = Environ.push_rel_context context (Global.env ()) in
+    let glob_body =
       GCases
 	(d0,RegularStyle,None,
 	 [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
@@ -1121,19 +1125,8 @@ let (value_f:constr list -> global_reference -> constr) =
 			       Anonymous)],
 	  GVar(d0,v_id)])
     in
-    let value =
-      List.fold_left2
-	(fun acc x_id a ->
-	   GLambda
-      	     (d0, Name x_id, Explicit, GDynamic(d0, constr_in a),
-	      acc
-	     )
-	)
-	fun_body
-	rev_x_id_l
-	(List.rev al)
-    in
-    understand Evd.empty (Global.env()) value;;
+    let body = understand Evd.empty env glob_body in
+    it_mkLambda_or_LetIn body context
 
 let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
   fun f_id kind value ->