Move the handling of the principal evar from refine to evd.

See previous commit for more discussion.

Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.

5 files changed, 83 insertions, 60 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ca6d26f617..dd74ecf384 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -360,36 +360,48 @@ let new_pure_evar_full evd evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ =
+let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ =
+  let default_naming =
+    if principal then
+        (* waiting for a more principled approach
+           (unnamed evars, private names?) *)
+        Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
+      else
+        Misctypes.IntroAnonymous
+  in
+  let naming = Option.default default_naming naming in
   let newevk = new_untyped_evar() in
   let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in
-  let evd = Evd.declare_future_goal newevk evd in
+  let evd =
+    if principal then Evd.declare_principal_goal newevk evd
+    else Evd.declare_future_goal newevk evd
+  in
   (evd,newevk)
 
-let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) instance =
+let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ~naming typ in
+  let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   (evd,mkEvar (newevk,Array.of_list instance))
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar env evd ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ =
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
   let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
   let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
   let instance =
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ~naming instance
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-let new_type_evar env evd ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid =
+let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
   let evd', s = new_sort_variable rigid evd in
-  let evd', e = new_evar env evd' ?src ?filter ~naming (mkSort s) in
+  let evd', e = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
     evd', (e, s)
 
-let e_new_type_evar env evdref ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid =
-  let evd', c = new_type_evar env !evdref ?src ?filter ~naming rigid in
+let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
+  let evd', c = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
     evdref := evd';
     c
 
@@ -402,8 +414,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
     evdref := evd'; mkSort s
 
   (* The same using side-effect *)
-let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) ty =
-  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ~naming ty in
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
+  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
   evdref := evd';
   ev
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f38c1ea0fb..ea00f80673 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -24,12 +24,14 @@ val mk_new_meta : unit -> constr
 val new_evar :
   env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * constr
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> evar_map * constr
 
 val new_pure_evar :
   named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * evar
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> evar_map * evar
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 
@@ -37,18 +39,19 @@ val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 val e_new_evar :
   env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> types -> constr
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
   env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> rigid ->
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
   evar_map * (constr * sorts)
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> constr * sorts
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
@@ -71,6 +74,7 @@ val new_evar_instance :
  named_context_val -> evar_map -> types -> 
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> 
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool ->
   constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c592ab9a54..35ca18e4f5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -585,8 +585,16 @@ type evar_map = {
   metas      : clbinding Metamap.t;
   (** Interactive proofs *)
   effects    : Declareops.side_effects;
-  future_goals : Evar.t list; (** list of newly created evars,
-                                  to be eventually turned into goals if not solved.*)
+  future_goals : Evar.t list; (** list of newly created evars, to be
+                                  eventually turned into goals if not solved.*)
+  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
+                                             contained
+                                             [future_goals]. The evar
+                                             [e] will inherit
+                                             properties (now: the
+                                             name) of the evar which
+                                             will be instantiated with
+                                             a term containing [e]. *)
 }
 
 (*** Lifting primitive from Evar.Map. ***)
@@ -796,6 +804,7 @@ let empty = {
   effects    = Declareops.no_seff;
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
   future_goals = [];
+  principal_future_goal = None;
 }
 
 let from_env ?ctx e = 
@@ -984,10 +993,19 @@ let eval_side_effects evd = evd.effects
 let declare_future_goal evk evd =
   { evd with future_goals = evk::evd.future_goals }
 
+let declare_principal_goal evk evd =
+  match evd.principal_future_goal with
+  | None -> { evd with
+    future_goals = evk::evd.future_goals;
+    principal_future_goal=Some evk; }
+  | Some _ -> Errors.error "Only one main subgoal per instantiation."
+
 let future_goals evd = evd.future_goals
 
+let principal_future_goal evd = evd.principal_future_goal
+
 let reset_future_goals evd =
-  { evd with future_goals = [] }
+  { evd with future_goals = [] ; principal_future_goal=None }
 
 let meta_diff ext orig = 
   Metamap.fold (fun m v acc ->
@@ -1445,6 +1463,7 @@ let set_metas evd metas = {
   effects = evd.effects;
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
+  principal_future_goal = evd.principal_future_goal;
 }
 
 let meta_list evd = metamap_to_list evd.metas
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 45432de36d..c15975b0ea 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -284,13 +284,22 @@ val declare_future_goal : Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
+val declare_principal_goal : Evar.t -> evar_map -> evar_map
+(** Adds an existential variable to the list of future goals and make
+    it principal. Only one existential variable can be made principal, an
+    error is raised otherwise. For internal uses only. *)
+
 val future_goals : evar_map -> Evar.t list
 (** Retrieves the list of future goals. Used by the [refine] primitive
     of the tactic engine. *)
 
+val principal_future_goal : evar_map -> Evar.t option
+(** Retrieves the name of the principal existential variable if there
+    is one. Used by the [refine] primitive of the tactic engine. *)
+
 val reset_future_goals : evar_map -> evar_map
-(** Clears the list of future goals. Used by the [refine] primitive of
-    the tactic engine. *)
+(** Clears the list of future goals (as well as the principal future
+    goal). Used by the [refine] primitive of the tactic engine. *)
 
 (** {5 Sort variables}
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 657f6bb2e9..cc380ed051 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -959,42 +959,24 @@ end
 
 module Refine =
 struct
-  type handle = Evd.evar_map * Evar.t option
-
-  let new_evar (evd, evkmain) ?(main=false) env typ =
-    let naming =
-      if main then
-        (* waiting for a more principled approach
-           (unnamed evars, private names?) *)
-        Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
-      else
-        Misctypes.IntroAnonymous in
-    let (evd, ev) = Evarutil.new_evar env evd ~naming typ in
-    let (evk, _) = Term.destEvar ev in
-    let evkmain =
-      if main then match evkmain with
-      | Some _ -> Errors.error "Only one main subgoal per instantiation."
-      | None -> Some evk
-      else evkmain in
-    let h = (evd, evkmain) in
-    (h, ev)
-
-  let new_evar_instance (evd, evkmain) ctx typ inst =
-    let (evd, ev) = Evarutil.new_evar_instance ctx evd typ inst in
-    let h = (evd, evkmain) in
-    (h, ev)
-
-  let fresh_constructor_instance (evd,evkmain) env construct =
-    let (evd,pconstruct) = Evd.fresh_constructor_instance env evd construct in
-    (evd,evkmain) , pconstruct
-
-  let with_type (evd,evkmain) env c t =
+  type handle = Evd.evar_map
+
+  let new_evar evd ?(main=false) env typ =
+    Evarutil.new_evar env evd ~principal:main typ
+
+  let new_evar_instance evd ctx typ inst =
+    Evarutil.new_evar_instance ctx evd typ inst
+
+  let fresh_constructor_instance evd env construct =
+    Evd.fresh_constructor_instance env evd construct
+
+  let with_type evd env c t =
     let my_type = Retyping.get_type_of env evd c in
     let j = Environ.make_judge c my_type in
     let (evd,j') =
       Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
     in
-    (evd,evkmain) , j'.Environ.uj_val
+    evd , j'.Environ.uj_val
 
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
@@ -1009,12 +991,12 @@ struct
     !evdref
 
   let refine ?(unsafe = false) f = Goal.enter begin fun gl ->
-    let sigma = Goal.sigma gl in
+    let sigma = Evd.reset_future_goals (Goal.sigma gl) in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
-    let handle = (Evd.reset_future_goals sigma, None) in
-    let ((sigma, evkmain), c) = f handle in
+    let (sigma, c) = f sigma in
     let evs = Evd.future_goals sigma in
+    let evkmain = Evd.principal_future_goal sigma in
     (** Check that the introduced evars are well-typed *)
     let fold accu ev = typecheck_evar ev env accu in
     let sigma = if unsafe then sigma else List.fold_left fold sigma evs in
@@ -1037,10 +1019,7 @@ struct
     refine ~unsafe f
   end
 
-  let update (evd, evkmain) f =
-    let nevd, ans = f evd in
-    (nevd, evkmain), ans
-
+  let update evd f = f evd
 end
 
 module NonLogical = Proofview_monad.NonLogical