Fix computation of obligations for mutually recursive definitions.

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

1 files changed, 11 insertions, 5 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3c85868d5..e45005ac3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -880,6 +880,11 @@ let out_def = function
   | Some def -> def
   | None -> error "Program Fixpoint needs defined bodies."
 
+let collect_evars_of_term evd c ty =
+  let evars = Intset.union (evars_of_term c) (evars_of_term ty) in
+    Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
+      evars Evd.empty
+      
 let do_program_recursive fixkind fixl ntns =
   let isfix = fixkind <> Obligations.IsCoFixpoint in
   let (env, rec_sign, evd), fix, info = 
@@ -889,17 +894,18 @@ let do_program_recursive fixkind fixl ntns =
     (* Get the interesting evars, those that were not instanciated *)
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
     (* Solve remaining evars *)
+  let evd = nf_evar_map_undefined evd in
   let rec collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
     let def =
-      Termops.it_mkNamedLambda_or_LetIn def rec_sign
+      nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
     and typ =
-      Termops.it_mkNamedProd_or_LetIn typ rec_sign
+      nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
     in
+    let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ = 
-      Obligations.eterm_obligations env id evd 
-	(List.length rec_sign) 
-	(nf_evar evd def) (nf_evar evd typ)
+      Obligations.eterm_obligations env id evm
+	(List.length rec_sign) def typ
     in (id, def, typ, imps, evars)
   in
   let (fixnames,fixdefs,fixtypes) = fix in