From c47916933025a4853ed0b397d7476b844bb894a4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 May 2015 14:44:10 +0200 Subject: STM/Univ: save initial univs (the ones in the statement) in Proof.proof This makes the treatment of universe constraints/normalization more understandable in the Sync/Async case: - if one has to keep the constraints of the body and the type of a lemma separate, then equations coming from the body are kept (see: 866c41 ) - if they can be merge then the equations (substituted on both the body and type) can be removed (one of the sides occurs nowhere) The result is that, semantically, the constraints of a lemma do not depend on weather it was produced asynchronously (v->vio->vo, or in a CoqIDE session) or synchronously (v->vo). Still the internal representation of the constraints changes to accommodate an optimization (to reduce the size of the constraint set): - in the synchronous case (some) equations are substituted (in both the type and body), hence they can be completely dropped from the constraint set - in the asynchronous case (some) equations are substituted in the body only (the type is fixed once and for all before the equations are discovered/generated), hence these equations are necessary to relate the type and the (optimized) body and are hence kept in the constraint set --- proofs/proof.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'proofs/proof.ml') diff --git a/proofs/proof.ml b/proofs/proof.ml index 828f9fa71..a7077d911 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -111,6 +111,8 @@ type proof = { shelf : Goal.goal list; (* List of goals that have been given up *) given_up : Goal.goal list; + (* The initial universe context (for the statement) *) + initial_euctx : Evd.evar_universe_context } (*** General proof functions ***) @@ -271,7 +273,9 @@ let start sigma goals = entry; focus_stack = [] ; shelf = [] ; - given_up = [] } in + given_up = []; + initial_euctx = + Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr let dependent_start goals = let entry, proofview = Proofview.dependent_init goals in @@ -280,7 +284,9 @@ let dependent_start goals = entry; focus_stack = [] ; shelf = [] ; - given_up = [] } in + given_up = []; + initial_euctx = + Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr @@ -311,6 +317,7 @@ let return p = Proofview.return p.proofview let initial_goals p = Proofview.initial_goals p.entry +let initial_euctx p = p.initial_euctx let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in -- cgit v1.2.3