1 files changed, 50 insertions, 74 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 316f02bc37..1f076470c1 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -31,7 +31,7 @@ type entry = (EConstr.constr * EConstr.types) list
     ide-s. *)
 (* spiwack: the type of [proofview] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: returns the list of focused goals together with
    the [evar_map] context. *)
 let proofview p =
@@ -46,7 +46,7 @@ let compact el ({ solution } as pv) =
   let apply_subst_einfo _ ei =
     Evd.({ ei with
        evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+       evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps;
        evar_candidates = Option.map (List.map nf) 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
@@ -114,7 +114,7 @@ type focus_context = goal_with_state list * goal_with_state list
     instance, ide-s. *)
 (* spiwack: the type of [focus_context] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. 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 (left,right) =
@@ -123,7 +123,7 @@ let focus_context (left,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
-    original list.  The focused list has lenght [j-i-1] and contains
+    original list.  The focused list has length [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
     [IndexOutOfRange] if [i > length l], or [j > length l] or [j <
@@ -245,7 +245,7 @@ let tclUNIT = Proof.return
 (** Bind operation of the tactic monad. *)
 let tclBIND = Proof.(>>=)
 
-(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation,
+(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
     it's a specialized "bind". *)
 let tclTHEN = Proof.(>>)
 
@@ -345,29 +345,19 @@ let tclBREAK = Proof.break
 
 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 -> Pp.t) ref = ref (fun n -> mt ())
-let set_nosuchgoals_hook f = nosuchgoals_hook := f
-
-
-
-(* This uses the hook above *)
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
-    let suffix = !nosuchgoals_hook n in
-    CErrors.user_err 
-      (str "No such " ++ str (String.plural n "goal") ++ str "." ++
-       pr_non_empty_arg (fun x -> x) suffix)
-      | _ -> raise CErrors.Unhandled
+    CErrors.user_err
+      (str "No such " ++ str (String.plural n "goal") ++ str ".")
+  | _ -> raise CErrors.Unhandled
 end
 
-(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
+(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
     only the goals numbered [i] to [j] are focused (the rest of the goals
     is restored at the end of the tactic). If the range [i]-[j] is not
     valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
-let tclFOCUS_gen nosuchgoal i j t =
+let tclFOCUS ?nosuchgoal i j t =
+  let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -378,41 +368,32 @@ let tclFOCUS_gen nosuchgoal i j t =
     return result
   with CList.IndexOutOfRange -> nosuchgoal
 
-let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
-let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
+let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
 
-let tclFOCUSLIST l t =
+let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t =
   let open Proof in
   Comb.get >>= fun comb ->
-    let n = CList.length comb in
-    (* First, remove empty intervals, and bound the intervals to the number
-       of goals. *)
-    let sanitize (i, j) =
-      if i > j then None
-      else if i > n then None
-      else if j < 1 then None
-      else Some ((max i 1), (min j n))
-    in
-    let l = CList.map_filter sanitize l in
+  let n = CList.length comb in
+  let ok (i, j) = 1 <= i && i <= j && j <= n in
+  if not (CList.for_all ok l) then nosuchgoal
+  else
     match l with
-      | [] -> tclZERO (NoSuchGoals 0)
-      | (mi, _) :: _ ->
-          (* Get the left-most goal to focus. This goal won't move, and we
-             will then place all the other goals to focus to the right. *)
-          let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
-          (* [CList.goto] returns a zipper, so that
-             [(rev left) @ sub_right = comb]. *)
-          let left, sub_right = CList.goto (mi-1) comb in
-          let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
-          let sub, right = CList.partitioni p sub_right in
-          let mj = mi - 1 + CList.length sub in
-            Comb.set (CList.rev_append left (sub @ right)) >>
-            tclFOCUS mi mj t
-
-
+    | [] -> nosuchgoal
+    | (mi, _) :: _ ->
+      (* Get the left-most goal to focus. This goal won't move, and we
+         will then place all the other goals to focus to the right. *)
+      let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
+      (* [CList.goto] returns a zipper, so that
+         [(rev left) @ sub_right = comb]. *)
+      let left, sub_right = CList.goto (mi-1) comb in
+      let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
+      let sub, right = CList.partitioni p sub_right in
+      let mj = mi - 1 + CList.length sub in
+      Comb.set (CList.rev_append left (sub @ right)) >>
+      tclFOCUS mi mj t
 
 (** Like {!tclFOCUS} but selects a single goal by name. *)
-let tclFOCUSID id t =
+let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -432,7 +413,7 @@ let tclFOCUSID id t =
         t >>= fun result ->
       Comb.set initial.comb  >>
         return result
-  with Not_found -> tclZERO (NoSuchGoals 1)
+  with Not_found -> nosuchgoal
 
 (** {7 Dispatching on goals} *)
 
@@ -561,7 +542,7 @@ let tclDISPATCHGEN join tacs =
   let tacs = CList.map branch tacs in
   InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
 
-let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs
+let tclDISPATCH tacs = tclDISPATCHGEN ignore tacs
 
 let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
 
@@ -652,7 +633,7 @@ let shelve_goals l =
     [sigma]. *)
 let depends_on sigma src tgt =
   let evi = Evd.find sigma tgt in
-  Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+  Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (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
@@ -868,7 +849,8 @@ let give_up =
 
 module Progress = struct
 
-  let eq_constr = Evarutil.eq_constr_univs_test
+  let eq_constr evd extended_evd =
+    Evarutil.eq_constr_univs_test ~evd ~extended_evd
 
   (** equality function on hypothesis contexts *)
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
@@ -898,10 +880,10 @@ module Progress = struct
     eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
 
   (** 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
-    eq_evar_info evars1 evars2 evi1 evi2
+  let goal_equal ~evd ~extended_evd evar extended_evar =
+    let evi = Evd.find evd evar in
+    let extended_evi = Evd.find extended_evd extended_evar in
+    eq_evar_info evd extended_evd evi extended_evi
 
 end
 
@@ -918,18 +900,18 @@ let tclPROGRESS t =
   let test =
     quick_test ||
     Util.List.for_all2eq begin fun i f ->
-      Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f)
+      Progress.goal_equal ~evd:initial.solution
+        ~extended_evd:final.solution (drop_state i) (drop_state f)
     end initial.comb final.comb
   in
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError (Some "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.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
-  | _ -> Pervasives.raise CErrors.Unhandled
+  | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | _ -> raise CErrors.Unhandled
 end
 
 let tclTIMEOUT n t =
@@ -953,7 +935,8 @@ let tclTIMEOUT n t =
       end
       begin let open Logic_monad.NonLogical in function (e, info) ->
         match e with
-        | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
+        | Logic_monad.Tac_Timeout ->
+          return (Util.Inr (Logic_monad.Tac_Timeout, info))
         | Logic_monad.TacticFailure e ->
           return (Util.Inr (e, info))
         | e -> Logic_monad.NonLogical.raise ~info e
@@ -1115,13 +1098,6 @@ module Goal = struct
         tclZERO ~info e
     end
     end
-
-  let normalize { self; state } =
-    Env.get >>= fun env ->
-    tclEVARMAP >>= fun sigma ->
-    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
@@ -1269,9 +1245,9 @@ module V82 = struct
     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 top_evars initial { solution=sigma; } =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+      Evar.Set.elements (Evd.evars_of_term sigma c)
     in
     CList.flatten (CList.map evars_of_initial initial)