From 2de8910d2cc0af096e6d91b0ea165997ce144503 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 2 May 2014 11:34:53 +0200
Subject: - Fix treatment of global universe constraints which should be passed
 along in the Evd of proofs (Evd.from_env). - Allow to set the Store.t value
 of new evars, e.g. to set constraint evars as unresolvable in rewrite.ml. -
 Fix a HUGE performance problem in the processing of constraints, which was
 remerging all the previous constraints with the ambient global universes at
 each new constraint addition. Performance is now back to (or better than)
 normal.

---
 toplevel/command.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index f4171da1b3..bc6f88e691 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -245,7 +245,7 @@ let declare_assumptions idl is_coe k c imps impl_is_on nl =
 
 let do_assumptions kind nl l =
   let env = Global.env () in
-  let evdref = ref Evd.empty in
+  let evdref = ref (Evd.from_env env) in
   let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
     let (t,ctx),imps = interp_assumption evdref env [] c in
     let env =
@@ -752,8 +752,8 @@ let nf_evar_context sigma ctx =
 
 let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
-  let evdref = ref Evd.empty in
   let env = Global.env() in
+  let evdref = ref (Evd.from_env env) in
   let _, ((env', binders_rel), impls) = interp_context_evars evdref env bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -892,7 +892,7 @@ let interp_recursive isfix fixl notations =
   let fixnames = List.map (fun fix -> fix.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
-  let evdref = ref Evd.empty in
+  let evdref = ref (Evd.from_env env) in
   let fixctxs, fiximppairs, fixannots =
     List.split3 (List.map (interp_fix_context evdref env isfix) fixl) in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
@@ -978,8 +978,10 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let env = Global.env() in
     let indexes = search_guard Loc.ghost env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
+    let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+    let ctx = Universes.restrict_universe_context ctx vars in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
     ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
-- 
cgit v1.2.3