Transfering the initial goals from the proofview to the proof object.

They were just passed along in the tactics.

6 files changed, 58 insertions, 66 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 10defd0f98..40e26e20a2 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -567,7 +567,6 @@ Extract Inlined Constant goal => "Goal.goal".
 Extract Inlined Constant env => "Environ.env".
 
 Record proofview := {
-  initial : list (constr*types);
   solution : evar_map;
   comb : list goal
 }.
diff --git a/proofs/proof.ml b/proofs/proof.ml
index aafacaeb3d..3d5eb20312 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -87,6 +87,8 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 type proof = {
   (* Current focused proofview *)
   proofview: Proofview.proofview;
+  (* Entry for the proofview *)
+  entry : Proofview.entry;
   (* History of the focusings, provides information on how
      to unfocus the proof and the extra information stored while focusing.
      The list is empty when the proof is fully unfocused. *)
@@ -131,7 +133,7 @@ let has_unresolved_evar p =
   Proofview.V82.has_unresolved_evar p.proofview
 
 (* Returns the list of partial proofs to initial goals *)
-let partial_proof p = Proofview.partial_proof p.proofview
+let partial_proof p = Proofview.partial_proof p.entry p.proofview
 
 (*** The following functions implement the basic internal mechanisms
      of proofs, they are not meant to be exported in the .mli ***)
@@ -227,19 +229,23 @@ let end_of_stack = CondEndStack end_of_stack_kind
 let unfocused = is_last_focus end_of_stack_kind
 
 let start sigma goals =
+  let entry, proofview = Proofview.init sigma goals in
   let pr = {
-    proofview = Proofview.init sigma goals ;
+    proofview;
+    entry;
     focus_stack = [] ;
     shelf = [] ;
     given_up = [] } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 let dependent_start sigma goals =
+  let entry, proofview = Proofview.dependent_init sigma goals in
   let pr = {
-    proofview = Proofview.dependent_init sigma goals ;
+    proofview;
+    entry;
     focus_stack = [] ;
     shelf = [] ;
     given_up = [] } in
-  let number_of_goals = List.length (Proofview.initial_goals pr.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
 
 exception UnfinishedProof
@@ -268,7 +274,7 @@ let return p =
     let p = unfocus end_of_stack_kind p () in
     Proofview.return p.proofview
 
-let initial_goals p = Proofview.initial_goals p.proofview
+let initial_goals p = Proofview.initial_goals p.entry
 
 (*** Function manipulation proof extra informations ***)
 
@@ -312,12 +318,12 @@ module V82 = struct
 
   let top_goal p =
     let { Evd.it=gls ; sigma=sigma; } =
-	Proofview.V82.top_goals p.proofview
+	Proofview.V82.top_goals p.entry p.proofview
     in
     { Evd.it=List.hd gls ; sigma=sigma; }
 
   let top_evars p =
-    Proofview.V82.top_evars p.proofview
+    Proofview.V82.top_evars p.entry
 
   let grab_evars p =
     if not (is_done p) then
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index c3a05b5227..aac11ffc4c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -26,6 +26,8 @@ open Util
 type proofview = Proofview_monad.proofview
 open Proofview_monad
 
+type entry = (Term.constr * Term.types) list
+
 let proofview p =
   p.comb , p.solution
 
@@ -33,25 +35,19 @@ let proofview p =
    conclusion types, and optional names, creating that many initial goals. *)
 let init sigma =
   let rec aux = function
-  | [] ->  { initial = [] ; 
-	     solution = sigma ;
-             comb = [];
-	   }
-  | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
-                           aux l
-                         in
-                         let ( new_defs , econstr ) = 
-			   Evarutil.new_evar sol env typ
-			 in
-			 let (e,_) = Term.destEvar econstr in
-			 let gl = Goal.build e in
-			 { initial = (econstr,typ)::ret;
-			   solution = new_defs ;
-                           comb = gl::comb; }
+  | [] ->  [], { solution = sigma; comb = []; }
+  | (env, typ) :: l ->
+    let ret, { solution = sol; comb = comb } = aux l in
+    let (new_defs , econstr) = Evarutil.new_evar sol env typ in
+    let (e, _) = Term.destEvar econstr in
+    let gl = Goal.build e in
+    let entry = (econstr, typ) :: ret in
+    entry, { solution = new_defs; comb = gl::comb; }
   in
-  fun l -> let v = aux l in
+  fun l ->
+    let entry, v = aux l in
     (* Marks all the goal unresolvable for typeclasses. *)
-    { v with solution = Typeclasses.mark_unresolvables v.solution }
+    entry, { v with solution = Typeclasses.mark_unresolvables v.solution }
 
 type telescope =
   | TNil
@@ -59,27 +55,21 @@ type telescope =
 
 let dependent_init =
   let rec aux sigma = function
-  | TNil -> { initial = [] ;
-	     solution = sigma ;
-             comb = [];
-	   }
-  | TCons (env,typ,t) -> let ( sigma , econstr ) =
-			  Evarutil.new_evar sigma env typ
-			in
-                        let { initial = ret ; solution = sol ; comb = comb } =
-                          aux sigma (t econstr)
-                        in
-			let (e,_) = Term.destEvar econstr in
-			let gl = Goal.build e in
-			{ initial = (econstr,typ)::ret;
-			   solution = sol ;
-                           comb = gl::comb; }
+  | TNil -> [], { solution = sigma; comb = []; }
+  | TCons (env, typ, t) ->
+    let (sigma, econstr ) = Evarutil.new_evar sigma env typ in
+    let ret, { solution = sol; comb = comb } = aux sigma (t econstr) in
+    let (e, _) = Term.destEvar econstr in
+    let gl = Goal.build e in
+    let entry = (econstr, typ) :: ret in
+    entry, { solution = sol; comb = gl :: comb; }
   in
-  fun sigma t -> let v = aux sigma t in
+  fun sigma t ->
+    let entry, v = aux sigma t in
     (* Marks all the goal unresolvable for typeclasses. *)
-    { v with solution = Typeclasses.mark_unresolvables v.solution }
+    entry, { v with solution = Typeclasses.mark_unresolvables v.solution }
 
-let initial_goals { initial } = initial
+let initial_goals initial = initial
 
 (* Returns whether this proofview is finished or not. That is,
    if it has empty subgoals in the comb. There could still be unsolved
@@ -93,8 +83,7 @@ let return { solution=defs } = defs
 
 let return_constr { solution = defs } c = Evarutil.nf_evar defs c
 
-let partial_proof pv =
-  List.map (return_constr pv) (List.map fst (initial_goals pv))
+let partial_proof entry pv = List.map (return_constr pv) (List.map fst entry)
 
 let emit_side_effects eff x =
   { x with solution = Evd.emit_side_effects eff x.solution }
@@ -513,9 +502,8 @@ let sensitive_on_proofview s env step =
   let ( new_defs , combed_subgoals ) = 
     List.fold_right wrap step.comb (step.solution,[])
   in
-  { step with
-     solution = new_defs;
-     comb = List.flatten combed_subgoals; }
+  { solution = new_defs; comb = List.flatten combed_subgoals; }
+
 let tclSENSITIVE s =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
@@ -675,7 +663,7 @@ module V82 = struct
       in
       let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
       let sgs = List.flatten goalss in
-      Proof.set { ps with solution=evd ; comb=sgs; }
+      Proof.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let e = Errors.push e in
       tclZERO e
@@ -687,7 +675,7 @@ module V82 = struct
     Proof.modify begin fun ps ->
     let map g s = Goal.V82.nf_evar s g in
     let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
-    { ps with solution=evd ; comb=goals }
+    { solution = evd; comb = goals; }
     end
 
   (* A [Proofview.tactic] version of [Refiner.tclEVARS] *)
@@ -714,11 +702,11 @@ module V82 = struct
   let goals { comb = comb ; solution = solution; } =
    { Evd.it = comb ; sigma = solution }
 
-  let top_goals { initial=initial ; solution=solution; } =
+  let top_goals initial { solution=solution; } =
     let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
-  let top_evars { initial=initial } =
+  let top_evars initial =
     let evars_of_initial (c,_) =
       Evar.Set.elements (Evarutil.evars_of_term c)
     in
@@ -740,7 +728,7 @@ module V82 = struct
 
   let of_tactic t gls =
     try
-      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
+      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
       let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
     with Proof_errors.TacticFailure e ->
@@ -858,7 +846,7 @@ struct
     let handle = (sigma, []) in
     let ((sigma, evs), c) = f handle in
     let sigma = partial_solution sigma gl.Goal.self c in
-    let modify start = { start with solution = sigma; comb = List.rev evs; } in
+    let modify start = { solution = sigma; comb = List.rev evs; } in
     Proof.modify modify
   end
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 436511f4a9..55d93f92e0 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -22,8 +22,7 @@
 
 open Term
 
-type proofview 
-
+type proofview
 
 (* Returns a stylised view of a proofview for use by, for instance,
    ide-s. *)
@@ -34,9 +33,11 @@ type proofview
    the [evar_map] context. *)
 val proofview : proofview -> Goal.goal list * Evd.evar_map
 
+type entry
+
 (* Initialises a proofview, the argument is a list of environement, 
    conclusion types, creating that many initial goals. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> proofview
+val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
 
 type telescope =
   | TNil
@@ -45,7 +46,7 @@ type telescope =
 (* Like [init], but goals are allowed to be depedenent on one
    another. Dependencies between goals is represented with the type
    [telescope] instead of [list]. *)
-val dependent_init  : Evd.evar_map -> telescope -> proofview
+val dependent_init  : Evd.evar_map -> telescope -> entry * proofview
 
 (* Returns whether this proofview is finished or not. That is,
    if it has empty subgoals in the comb. There could still be unsolved
@@ -55,8 +56,8 @@ val finished : proofview -> bool
 (* Returns the current value of the proofview partial proofs. *)
 val return : proofview -> Evd.evar_map
 
-val partial_proof : proofview -> constr list
-val initial_goals : proofview -> (constr * types) list
+val partial_proof : entry -> proofview -> constr list
+val initial_goals : entry -> (constr * types) list
 val emit_side_effects : Declareops.side_effects -> proofview -> proofview
 
 (*** Focusing operations ***)
@@ -308,10 +309,10 @@ module V82 : sig
      interprete them. *)
   val goals : proofview -> Goal.goal list Evd.sigma
 
-  val top_goals : proofview -> Goal.goal list Evd.sigma
+  val top_goals : entry -> proofview -> Goal.goal list Evd.sigma
   
   (* returns the existential variable used to start the proof *)
-  val top_evars : proofview -> Evd.evar list
+  val top_evars : entry -> Evd.evar list
     
   (* Implements the Existential command *)
   val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 80ab416425..8008e108b3 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -90,8 +90,7 @@ module IOBase =
  
  end
 
-type proofview = { initial : (Term.constr*Term.types) list;
-                   solution : Evd.evar_map; comb : Goal.goal list }
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
 
 type logicalState = proofview
 
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 26c6a301e6..6a832e40f5 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -5,8 +5,7 @@ type ('a, 'b) list_view =
 | Nil of exn
 | Cons of 'a * 'b
 
-type proofview = { initial : (Term.constr * Term.types) list;
-                   solution : Evd.evar_map; comb : Goal.goal list }
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
 
 type logicalState = proofview