Merge PR #8892: Fix part of #8224: grounding open term in fixpoints

3 files changed, 25 insertions, 9 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 138696e3a7..a9c499b192 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -99,7 +99,7 @@ let check_mutuality env evd isfix fixl =
   let names = List.map fst fixl in
   let preorder =
     List.map (fun (id,def) ->
-      (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names))
+      (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names))
       fixl in
   let po = partial_order Id.equal preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
@@ -227,25 +227,28 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   (* Instantiate evars and check all are resolved *)
   let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
   let sigma = Evd.minimize_universes sigma in
-  (* XXX: We still have evars here in Program *)
-  let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in
-  let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
   (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
-  check_evars_are_solved env evd (Evd.from_env env);
   if List.for_all Option.has_some fixdefs then begin
     let fixdefs = List.map Option.get fixdefs in
     check_mutuality env evd isfix (List.combine fixnames fixdefs)
   end
 
+let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) =
+  check_evars_are_solved env evd (Evd.from_env env);
+  let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
+  let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
+  Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes)
+
 let interp_fixpoint ~cofix l ntns =
   let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in
   check_recursive true env evd fix;
-  (fix,pl,Evd.evar_universe_context evd,info)
+  let uctx,fix = ground_fixpoint env evd fix in
+  (fix,pl,uctx,info)
 
 let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index b1a9c8a5a3..f4569ed3e2 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -51,7 +51,7 @@ val interp_recursive :
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
-  (Id.t list * Constr.constr option list * Constr.types list) *
+  (Id.t list * EConstr.constr option list * EConstr.types list) *
   (* ctx per mutual def / implicits / struct annotations *)
   (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index d533db7ed9..ebedfb1e0d 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open Pp
 open CErrors
 open Util
@@ -251,10 +261,10 @@ let do_program_recursive local poly fixkind fixl ntns =
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
     let def =
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
+      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
     and typ =
       (* Worrying... *)
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
+      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
     in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
@@ -268,6 +278,9 @@ let do_program_recursive local poly fixkind fixl ntns =
   let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
   let () = if not cofix then begin
       let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in
+      (* XXX: are we allowed to have evars here? *)
+      let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in
+      let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in
       let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
         Array.of_list fixtypes,
         Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)