1 files changed, 210 insertions, 156 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index c0187976..22271dd0 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 
@@ -16,13 +18,14 @@
 open Pp
 open Util
 open Proofview_monad
-open Sigma.Notations
 open Context.Named.Declaration
 
 (** Main state of tactics *)
 type proofview = Proofview_monad.proofview
 
-type entry = (Term.constr * Term.types) list
+(* The first items in pairs below are proofs (under construction).
+   The second items in the pairs below are statements that are being proved. *)
+type entry = (EConstr.constr * EConstr.types) list
 
 (** Returns a stylised view of a proofview for use by, for instance,
     ide-s. *)
@@ -32,18 +35,19 @@ type entry = (Term.constr * Term.types) list
 (* In this version: returns the list of focused goals together with
    the [evar_map] context. *)
 let proofview p =
-  p.comb , p.solution
+  List.map drop_state p.comb , p.solution
 
 let compact el ({ solution } as pv) =
-  let nf = Evarutil.nf_evar solution in
+  let nf c = Evarutil.nf_evar solution c in
+  let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
   let pruned_solution = Evd.drop_all_defined solution in
   let apply_subst_einfo _ ei =
     Evd.({ ei with
-       evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf ei.evar_hyps;
-       evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
+       evar_concl =  nf0 ei.evar_concl;
+       evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+       evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
@@ -54,7 +58,7 @@ let compact el ({ solution } as pv) =
 
 type telescope =
   | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
+  | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
 let typeclass_resolvable = Evd.Store.field ()
 
@@ -63,18 +67,16 @@ let dependent_init =
      for type classes. *)
   let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in
   (* Goals don't have a source location. *)
-  let src = (Loc.ghost,Evar_kinds.GoalEvar) in
+  let src = Loc.tag @@ Evar_kinds.GoalEvar in
   (* Main routine *)
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
-    let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
-    let sigma = Sigma.to_evar_map sigma in
+    let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in
+    let (gl, _) = EConstr.destEvar sigma econstr in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
-    let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
-    entry, { solution = sol; comb = gl :: comb; shelf = [] }
+    entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
   in
   fun t ->
     let entry, v = aux t in
@@ -110,7 +112,7 @@ let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry)
 (* First component is a reverse list of the goals which come before
    and second component is the list of the goals which go after (in
    the expected order). *)
-type focus_context = Evar.t list * Evar.t list
+type focus_context = goal_with_state list * goal_with_state list
 
 
 (** Returns a stylised view of a focus_context for use by, for
@@ -120,11 +122,12 @@ type focus_context = Evar.t list * Evar.t list
    new nearly identical function everytime. Hence the generic name. *)
 (* In this version: the goals in the context, as a "zipper" (the first
    list is in reversed order). *)
-let focus_context f = f
+let focus_context (left,right) =
+  (List.map drop_state left, List.map drop_state right)
 
 (** This (internal) function extracts a sublist between two indices,
     and returns this sublist together with its context: if it returns
-    [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the
+    [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the
     original list.  The focused list has lenght [j-i-1] and contains
     the goals from number [i] to number [j] (both included) the first
     goal of the list being numbered [1].  [focus_sublist i j l] raises
@@ -149,17 +152,35 @@ let unfocus_sublist (left,right) s =
     proofview.  It returns the focused proofview, and a context for
     the focus stack. *)
 let focus i j sp =
-  let (new_comb, context) = focus_sublist i j sp.comb in
-  ( { sp with comb = new_comb } , context )
+  let (new_comb, (left, right)) = focus_sublist i j sp.comb in
+  ( { sp with comb = new_comb } , (left, right) )
+
+let cleared_alias evd g =
+  let evk = drop_state g in
+  let state = get_state g in
+  Option.map (fun g -> goal_with_state g state) (Evarutil.advance evd evk)
 
 (** [undefined defs l] is the list of goals in [l] which are still
-    unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (Evarutil.advance defs) l
+    unsolved (after advancing cleared goals). Note that order matters. *)
+let undefined_evars defs l =
+  List.fold_right (fun evk l ->
+      match Evarutil.advance defs evk with
+      | Some evk -> List.add_set Evar.equal evk l
+      | None -> l) l []
+let goal_with_state_equal x y = Evar.equal (drop_state x) (drop_state y)
+let undefined defs l =
+  List.fold_right (fun evk l ->
+      match cleared_alias defs evk with
+      | Some evk -> List.add_set goal_with_state_equal evk l
+      | None -> l) l []
 
 (** Unfocuses a proofview with respect to a context. *)
-let unfocus c sp =
-  { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
+let unfocus (left, right) sp =
+  { sp with comb = undefined sp.solution (unfocus_sublist (left, right) sp.comb) }
 
+let with_empty_state = Proofview_monad.with_empty_state
+let drop_state = Proofview_monad.drop_state
+let goal_with_state = Proofview_monad.goal_with_state
 
 (** {6 The tactic monad} *)
 
@@ -286,7 +307,7 @@ let tclONCE = Proof.once
 
 exception MoreThanOneSuccess
 let _ = CErrors.register_handler begin function
-  | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success."
+  | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -332,7 +353,7 @@ exception NoSuchGoals of int
 (* This hook returns a string to be appended to the usual message.
    Primarily used to add a suggestion about the right bullet to use to
    focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ())
+let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ())
 let set_nosuchgoals_hook f = nosuchgoals_hook := f
 
 
@@ -341,7 +362,7 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
     let suffix = !nosuchgoals_hook n in
-    CErrors.errorlabstrm ""
+    CErrors.user_err 
       (str "No such " ++ str (String.plural n "goal") ++ str "." ++
        pr_non_empty_arg (fun x -> x) suffix)
       | _ -> raise CErrors.Unhandled
@@ -402,7 +423,8 @@ let tclFOCUSID id t =
   try
     let ev = Evd.evar_key id initial.solution in
     try
-      let n = CList.index Evar.equal ev initial.comb in
+      let comb = CList.map drop_state initial.comb in
+      let n = CList.index Evar.equal ev comb in
       (* goal is already under focus *)
       let (focused,context) = focus n n initial in
       Pv.set focused >>
@@ -411,7 +433,7 @@ let tclFOCUSID id t =
         return result
     with Not_found ->
       (* otherwise, save current focus and work purely on the shelve *)
-      Comb.set [ev] >>
+      Comb.set [with_empty_state ev] >>
         t >>= fun result ->
       Comb.set initial.comb  >>
         return result
@@ -421,13 +443,13 @@ let tclFOCUSID id t =
 
 exception SizeMismatch of int*int
 let _ = CErrors.register_handler begin function
-  | SizeMismatch (i,_) ->
+  | SizeMismatch (i,j) ->
       let open Pp in
       let errmsg =
         str"Incorrect number of goals" ++ spc() ++
-        str"(expected "++int i++str(String.plural i " tactic") ++ str")."
+        str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
       in
-      CErrors.errorlabstrm "" errmsg
+      CErrors.user_err  errmsg
   | _ -> raise CErrors.Unhandled
 end
 
@@ -441,7 +463,7 @@ let iter_goal i =
   Comb.get >>= fun initial ->
   Proof.List.fold_left begin fun (subgoals as cur) goal ->
     Solution.get >>= fun step ->
-    match Evarutil.advance step goal with
+    match cleared_alias step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -451,6 +473,25 @@ let iter_goal i =
   Solution.get >>= fun evd ->
   Comb.set CList.(undefined evd (flatten (rev subgoals)))
 
+(** List iter but allocates a list of results *)
+let map_goal i =
+  let rev = List.rev in (* hem... Proof masks List... *)
+  let open Proof in
+  Comb.get >>= fun initial ->
+  Proof.List.fold_left begin fun (acc, subgoals as cur) goal ->
+    Solution.get >>= fun step ->
+    match cleared_alias step goal with
+    | None -> return cur
+    | Some goal ->
+        Comb.set [goal] >>
+        i goal >>= fun res ->
+        Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x ->
+        return (res :: acc, x)
+  end ([],[]) initial >>= fun (results_rev, subgoals) ->
+  Solution.get >>= fun evd ->
+  Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
+  return (rev results_rev)
+
 (** A variant of [Monad.List.fold_left2] where the first list is the
     list of focused goals. The argument tactic is executed in a focus
     comprising only of the current goal, a goal which has been solved
@@ -465,7 +506,7 @@ let fold_left2_goal i s l =
   in 
   Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
     Solution.get >>= fun step ->
-    match Evarutil.advance step goal with
+    match cleared_alias step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -509,7 +550,7 @@ let tclDISPATCHGEN0 join tacs =
         let open Proof in
         Pv.get >>= function
         | { comb=[goal] ; solution } ->
-            begin match Evarutil.advance solution goal with
+            begin match cleared_alias solution goal with
             | None -> tclUNIT (join [])
             | Some _ -> Proof.map (fun res -> join [res]) tac
             end
@@ -531,8 +572,8 @@ let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
 
 
 (** [extend_to_list startxs rx endxs l] builds a list
-    [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises
-    [SizeMismatch] if [startxs@endxs] is already longer than [l]. *)
+    [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises
+    [SizeMismatch] if [startxs @ endxs] is already longer than [l]. *)
 let extend_to_list startxs rx endxs l =
   (* spiwack: I use [l] essentially as a natural number *)
   let rec duplicate acc = function
@@ -583,7 +624,15 @@ let tclINDEPENDENT tac =
       let tac = InfoL.tag (Info.DBranch) tac in
       InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
 
-
+let tclINDEPENDENTL tac =
+  let open Proof in
+  Pv.get >>= fun initial ->
+  match initial.comb with
+  | [] -> tclUNIT []
+  | [_] -> tac >>= fun x -> return [x]
+  | _ ->
+      let tac = InfoL.tag (Info.DBranch) tac in
+      InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac))
 
 (** {7 Goal manipulation} *)
 
@@ -593,42 +642,70 @@ let shelve =
   Comb.get >>= fun initial ->
   Comb.set [] >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
-  Shelf.modify (fun gls -> gls @ initial)
+  Shelf.modify (fun gls -> gls @ CList.map drop_state initial)
 
 let shelve_goals l =
   let open Proof in
   Comb.get >>= fun initial ->
-  let comb = CList.filter (fun g -> not (CList.mem g l)) initial in
+  let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
   Comb.set comb >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >>
   Shelf.modify (fun gls -> gls @ l)
 
-(** [contained_in_info e evi] checks whether the evar [e] appears in
-    the hypotheses, the conclusion or the body of the evar_info
-    [evi]. Note: since we want to use it on goals, the body is actually
-    supposed to be empty. *)
-let contained_in_info sigma e evi =
-  Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
-
 (** [depends_on sigma src tgt] checks whether the goal [src] appears
     as an existential variable in the definition of the goal [tgt] in
     [sigma]. *)
 let depends_on sigma src tgt =
   let evi = Evd.find sigma tgt in
-  contained_in_info sigma src evi
+  Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+
+let unifiable_delayed g l =
+  CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l
+
+let free_evars sigma l =
+  let cache = Evarutil.create_undefined_evars_cache () in
+  let map ev =
+  (** Computes the set of evars appearing in the hypotheses, the conclusion or
+      the body of the evar_info [evi]. Note: since we want to use it on goals,
+      the body is actually supposed to be empty. *)
+    let evi = Evd.find sigma ev in
+    let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
+    (ev, fevs)
+  in
+  List.map map l
+
+let free_evars_with_state sigma l =
+  let cache = Evarutil.create_undefined_evars_cache () in
+  let map ev =
+  (** Computes the set of evars appearing in the hypotheses, the conclusion or
+      the body of the evar_info [evi]. Note: since we want to use it on goals,
+      the body is actually supposed to be empty. *)
+    let ev = drop_state ev in
+    let evi = Evd.find sigma ev in
+    let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
+    (ev, fevs)
+  in
+  List.map map l
+
 
 (** [unifiable sigma g l] checks whether [g] appears in another
     subgoal of [l]. The list [l] may contain [g], but it does not
     affect the result. *)
+let unifiable_delayed_with_state sigma g l =
+  let g = drop_state g in
+  unifiable_delayed g l
+
 let unifiable sigma g l =
-  CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) l
+  let l = free_evars sigma l in
+  unifiable_delayed g l
 
 (** [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
     where [u] is composed of the unifiable goals, i.e. the goals on
     whose definition other goals of [l] depend, and [n] are the
     non-unifiable goals. *)
 let partition_unifiable sigma l =
-  CList.partition (fun g -> unifiable sigma g l) l
+  let fevs = free_evars_with_state sigma l in
+  CList.partition (fun g -> unifiable_delayed_with_state sigma g fevs) l
 
 (** Shelves the unifiable goals under focus, i.e. the goals which
     appear in other goals under focus (the unfocused goals are not
@@ -639,7 +716,7 @@ let shelve_unifiable =
   let (u,n) = partition_unifiable initial.solution initial.comb in
   Comb.set n >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
-  Shelf.modify (fun gls -> gls @ u)
+  Shelf.modify (fun gls -> gls @ CList.map drop_state u)
 
 (** [guard_no_unifiable] returns the list of unifiable goals if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
@@ -650,13 +727,14 @@ let guard_no_unifiable =
   match u with
   | [] -> tclUNIT None
   | gls ->
-      let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in
+      let l = CList.map (fun g -> Evd.dependent_evar_ident (drop_state g) initial.solution) gls in
       let l = CList.map (fun id -> Names.Name id) l in
       tclUNIT (Some l)
 
 (** [unshelve l p] adds all the goals in [l] at the end of the focused
     goals of p *)
 let unshelve l p =
+  let l = List.map with_empty_state l in
   (* advance the goals in case of clear *)
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
@@ -666,6 +744,12 @@ let mark_in_evm ~goal evd content =
   let info =
     if goal then
       { info with Evd.evar_source = match info.Evd.evar_source with
+            (* Two kinds for goal evars:
+               - GoalEvar (morally not dependent)
+               - VarInstance (morally dependent of some name).
+               This is a heuristic for naming these evars. *)
+            | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+                    Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
             | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
             | loc,_ -> loc,Evar_kinds.GoalEvar }
     else info
@@ -684,12 +768,13 @@ let with_shelf tac =
   tac >>= fun ans ->
   Pv.get >>= fun npv ->
   let { shelf = gls; solution = sigma } = npv in
+  (* The pending future goals are necessarily coming from V82.tactic *)
+  (* and thus considered as to shelve, as in Proof.run_tactic *)
   let gls' = Evd.future_goals sigma in
-  let fgoals = Evd.future_goals solution in
-  let pgoal = Evd.principal_future_goal solution in
-  let sigma = Evd.restore_future_goals sigma fgoals pgoal in
+  let fgoals = Evd.save_future_goals solution in
+  let sigma = Evd.restore_future_goals sigma fgoals in
   (* Ensure we mark and return only unsolved goals *)
-  let gls' = undefined sigma (CList.rev_append gls' gls) in
+  let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
   let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
   let npv = { npv with shelf; solution = sigma } in
   Pv.set npv >> tclUNIT (gls', ans)
@@ -771,7 +856,7 @@ let give_up =
   Comb.set [] >>
   mark_as_unsafe >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
-  Giveup.put initial
+  Giveup.put (CList.map drop_state initial)
 
 
 
@@ -812,8 +897,8 @@ module Progress = struct
 
   (** Equality function on goals *)
   let goal_equal evars1 gl1 evars2 gl2 =
-    let evi1 = Evd.find evars1 gl1 in
-    let evi2 = Evd.find evars2 gl2 in
+    let evi1 = Evd.find evars1 (drop_state gl1) in
+    let evi2 = Evd.find evars2 (drop_state gl2) in
     eq_evar_info evars1 evars2 evi1 evi2
 
 end
@@ -828,22 +913,20 @@ let tclPROGRESS t =
   let quick_test =
     initial.solution == final.solution && initial.comb == final.comb
   in
-  let exhaustive_test =
+  let test =
+    quick_test ||
     Util.List.for_all2eq begin fun i f ->
       Progress.goal_equal initial.solution i final.solution f
     end initial.comb final.comb
   in
-  let test =
-    quick_test || exhaustive_test
-  in
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
+    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
 
 exception Timeout
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> Pervasives.raise CErrors.Unhandled
 end
 
@@ -929,6 +1012,15 @@ module Unsafe = struct
 
   let tclSETGOALS = Comb.set
 
+  let tclGETSHELF = Shelf.get
+
+  let tclSETSHELF = Shelf.set
+
+  let tclPUTSHELF to_shelve =
+    tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf))
+
+  let tclPUTGIVENUP = Giveup.put
+
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
@@ -978,64 +1070,68 @@ let catchable_exception = function
 
 module Goal = struct
 
-  type ('a, 'r) t = {
+  type t = {
     env : Environ.env;
     sigma : Evd.evar_map;
-    concl : Term.constr ;
+    concl : EConstr.constr ;
+    state : StateStore.t;
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  type ('a, 'b) enter =
-    { enter : 'r. ('a, 'r) t -> 'b }
-
-  let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
+  let assume (gl : t) = (gl : t)
 
-  let env { env=env } = env
-  let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
-  let hyps { env=env } = Environ.named_context env
-  let concl { concl=concl } = concl
-  let extra { sigma=sigma; self=self } = goal_extra sigma self
+  let print { sigma; self } = { Evd.it = self; sigma }
 
-  let raw_concl { concl=concl } = concl
+  let state { state=state } = state
 
+  let env {env} = env
+  let sigma {sigma} = sigma
+  let hyps {env} = EConstr.named_context env
+  let concl {concl} = concl
+  let extra {sigma; self} = goal_extra sigma self
 
-  let gmake_with info env sigma goal = 
+  let gmake_with info env sigma goal state =
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
       sigma = sigma ;
-      concl = Evd.evar_concl info ;
+      concl = EConstr.of_constr (Evd.evar_concl info);
+      state = state ;
       self = goal }
 
   let nf_gmake env sigma goal =
+    let state = get_state goal in
+    let goal = drop_state goal in
     let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in
     let sigma = Evd.add sigma goal info in
-    gmake_with info env sigma goal , sigma
+    gmake_with info env sigma goal state , sigma
 
   let nf_enter f =
     InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
-      Env.get >>= fun env ->
+      tclENV >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl))
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
       with e when catchable_exception e ->
         let (e, info) = CErrors.push e in
         tclZERO ~info e
     end
     end
 
-  let normalize { self } =
+  let normalize { self; state } =
     Env.get >>= fun env ->
     tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = nf_gmake env sigma self in
+    let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
     tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
 
   let gmake env sigma goal =
+    let state = get_state goal in
+    let goal = drop_state goal in
     let info = Evd.find sigma goal in
-    gmake_with info env sigma goal
+    gmake_with info env sigma goal state
 
   let enter f =
-    let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in
+    let f gl = InfoL.tag (Info.DBranch) (f gl) in
     InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
       Env.get >>= fun env ->
@@ -1047,66 +1143,25 @@ module Goal = struct
     end
     end
 
-  exception NotExactlyOneSubgoal
-  let _ = CErrors.register_handler begin function
-  | NotExactlyOneSubgoal ->
-      CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.")
-  | _ -> raise CErrors.Unhandled
-  end
-
-  let enter_one f =
+  let enter_one ?(__LOC__=__LOC__) f =
     let open Proof in
     Comb.get >>= function
     | [goal] -> begin
        Env.get >>= fun env ->
        tclEVARMAP >>= fun sigma ->
-       try f.enter (gmake env sigma goal)
+       try f (gmake env sigma goal)
        with e when catchable_exception e ->
          let (e, info) = CErrors.push e in
          tclZERO ~info e
       end
-    | _ -> tclZERO NotExactlyOneSubgoal
-
-  type ('a, 'b) s_enter =
-    { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
-
-  let s_enter f =
-    InfoL.tag (Info.Dispatch) begin
-    iter_goal begin fun goal ->
-      Env.get >>= fun env ->
-      tclEVARMAP >>= fun sigma ->
-      try
-        let gl = gmake env sigma goal in
-        let Sigma (tac, sigma, _) = f.s_enter gl in
-        let sigma = Sigma.to_evar_map sigma in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
-      with e when catchable_exception e ->
-        let (e, info) = CErrors.push e in
-        tclZERO ~info e
-    end
-    end
-
-  let nf_s_enter f =
-    InfoL.tag (Info.Dispatch) begin
-    iter_goal begin fun goal ->
-      Env.get >>= fun env ->
-      tclEVARMAP >>= fun sigma ->
-      try
-        let (gl, sigma) = nf_gmake env sigma goal in
-        let Sigma (tac, sigma, _) = f.s_enter gl in
-        let sigma = Sigma.to_evar_map sigma in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
-      with e when catchable_exception e ->
-        let (e, info) = CErrors.push e in
-        tclZERO ~info e
-    end
-    end
+    | _ ->
+       CErrors.anomaly Pp.(str __LOC__ ++ str " enter_one")
 
   let goals =
     Pv.get >>= fun step ->
     let sigma = step.solution in
     let map goal =
-      match Evarutil.advance sigma goal with
+      match cleared_alias sigma goal with
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =
@@ -1125,8 +1180,6 @@ module Goal = struct
   (* compatibility *)
   let goal { self=self } = self
 
-  let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t)
-
 end
 
 
@@ -1161,25 +1214,29 @@ let tclCHECKINTERRUPT =
 module V82 = struct
   type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
 
-  let tactic tac =
+  let tactic ?(nf_evars=true) tac =
     (* spiwack: we ignore the dependencies between goals here,
        expectingly preserving the semantics of <= 8.2 tactics *)
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
     let open Proof in
     Pv.get >>= fun ps ->
     try
-      let tac gl evd = 
+      let tac g_w_s evd =
+        let g, w = drop_state g_w_s, get_state g_w_s in
         let glsigma  =
-          tac { Evd.it = gl ; sigma = evd; }  in
+          tac { Evd.it = g ; sigma = evd; }  in
         let sigma = glsigma.Evd.sigma in
-        let g = glsigma.Evd.it in
+        let g = CList.map (fun g -> goal_with_state g w) glsigma.Evd.it in
         ( g, sigma )
       in
         (* Old style tactics expect the goals normalized with respect to evars. *)
-      let (initgoals,initevd) =
-        Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution
+      let (initgoals_w_state, initevd) =
+        Evd.Monad.List.map (fun g_w_s s ->
+          let g, w = drop_state g_w_s, get_state g_w_s in
+          let g, s = if nf_evars then goal_nf_evar s g else g, s in
+          goal_with_state g w, s) ps.comb ps.solution
       in
-      let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
+      let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in
       let sgs = CList.flatten goalss in
       let sgs = undefined evd sgs in
       InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
@@ -1194,8 +1251,9 @@ module V82 = struct
   let nf_evar_goals =
     Pv.modify begin fun ps ->
     let map g s = goal_nf_evar s g in
-    let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
-    { ps with solution = evd; comb = goals; }
+    let comb = CList.map drop_state ps.comb in
+    let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in
+    { ps with solution = evd; }
     end
       
   let has_unresolved_evar pv =
@@ -1205,30 +1263,30 @@ module V82 = struct
   let grab pv =
     let undef = Evd.undefined_map pv.solution in
     let goals = CList.rev_map fst (Evar.Map.bindings undef) in
-    { pv with comb = goals }
+    { pv with comb = List.map with_empty_state goals }
       
     
 
   (* Returns the open goals of the proofview together with the evar_map to 
      interpret them. *)
   let goals { comb = comb ; solution = solution; } =
-   { Evd.it = comb ; sigma = solution }
+   { Evd.it = List.map drop_state comb ; sigma = solution }
 
   let top_goals initial { solution=solution; } =
-    let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in
+    let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
   let top_evars initial =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term c)
+      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
     in
     CList.flatten (CList.map evars_of_initial initial)
 
   let of_tactic t gls =
     try
-      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
+      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
       let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
-      { Evd.sigma = final.solution ; it = final.comb }
+      { Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
     with Logic_monad.TacticFailure e as src ->
       let (_, info) = CErrors.push src in
       iraise (e, info)
@@ -1250,8 +1308,4 @@ module Notations = struct
   let (>>=) = tclBIND
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-  type ('a, 'b) enter = ('a, 'b) Goal.enter =
-    { enter : 'r. ('a, 'r) Goal.t -> 'b }
-  type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter =
-    { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma }
 end