Moving Evarutil and Proofview to engine/

5 files changed, 0 insertions, 2746 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
deleted file mode 100644
index 2bd67dcdc..000000000
--- a/pretyping/evarutil.ml
+++ /dev/null
@@ -1,723 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Errors
-open Util
-open Pp
-open Names
-open Term
-open Vars
-open Termops
-open Namegen
-open Pre_env
-open Environ
-open Evd
-open Sigma.Notations
-
-let safe_evar_value sigma ev =
-  try Some (Evd.existential_value sigma ev)
-  with NotInstantiatedEvar | Not_found -> None
-
-(** Combinators *)
-
-let evd_comb0 f evdref =
-  let (evd',x) = f !evdref in
-    evdref := evd';
-    x
-
-let evd_comb1 f evdref x =
-  let (evd',y) = f !evdref x in
-    evdref := evd';
-    y
-
-let evd_comb2 f evdref x y =
-  let (evd',z) = f !evdref x y in
-    evdref := evd';
-    z
-
-let e_new_global evdref x = 
-  evd_comb1 (Evd.fresh_global (Global.env())) evdref x
-
-let new_global evd x = 
-  Sigma.fresh_global (Global.env()) evd x
-
-(****************************************************)
-(* Expanding/testing/exposing existential variables *)
-(****************************************************)
-
-(* flush_and_check_evars fails if an existential is undefined *)
-
-exception Uninstantiated_evar of existential_key
-
-let rec flush_and_check_evars sigma c =
-  match kind_of_term c with
-  | Evar (evk,_ as ev) ->
-      (match existential_opt_value sigma ev with
-       | None -> raise (Uninstantiated_evar evk)
-       | Some c -> flush_and_check_evars sigma c)
-  | _ -> map_constr (flush_and_check_evars sigma) c
-
-(* let nf_evar_key = Profile.declare_profile "nf_evar"  *)
-(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
-
-let rec whd_evar sigma c =
-  match kind_of_term c with
-    | Evar ev ->
-        let (evk, args) = ev in
-        let args = Array.map (fun c -> whd_evar sigma c) args in
-        (match safe_evar_value sigma (evk, args) with
-            Some c -> whd_evar sigma c
-          | None -> c)
-    | Sort (Type u) -> 
-      let u' = Evd.normalize_universe sigma u in
-	if u' == u then c else mkSort (Sorts.sort_of_univ u')
-    | Const (c', u) when not (Univ.Instance.is_empty u) -> 
-      let u' = Evd.normalize_universe_instance sigma u in
-	if u' == u then c else mkConstU (c', u')
-    | Ind (i, u) when not (Univ.Instance.is_empty u) -> 
-      let u' = Evd.normalize_universe_instance sigma u in
-	if u' == u then c else mkIndU (i, u')
-    | Construct (co, u) when not (Univ.Instance.is_empty u) ->
-      let u' = Evd.normalize_universe_instance sigma u in
-	if u' == u then c else mkConstructU (co, u')
-    | _ -> c
-
-let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t)
-
-let j_nf_evar sigma j =
-  { uj_val = nf_evar sigma j.uj_val;
-    uj_type = nf_evar sigma j.uj_type }
-let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
-let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
-let tj_nf_evar sigma {utj_val=v;utj_type=t} =
-  {utj_val=nf_evar sigma v;utj_type=t}
-
-let nf_evars_universes evm =
-  Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
-    (Evd.universe_subst evm)
-    
-let nf_evars_and_universes evm =
-  let evm = Evd.nf_constraints evm in
-    evm, nf_evars_universes evm
-
-let e_nf_evars_and_universes evdref =
-  evdref := Evd.nf_constraints !evdref;
-  nf_evars_universes !evdref, Evd.universe_subst !evdref
-
-let nf_evar_map_universes evm =
-  let evm = Evd.nf_constraints evm in
-  let subst = Evd.universe_subst evm in
-    if Univ.LMap.is_empty subst then evm, nf_evar evm
-    else
-      let f = nf_evars_universes evm in
-	Evd.raw_map (fun _ -> map_evar_info f) evm, f
-
-let nf_named_context_evar sigma ctx =
-  Context.Named.map (nf_evar sigma) ctx
-
-let nf_rel_context_evar sigma ctx =
-  Context.Rel.map (nf_evar sigma) ctx
-
-let nf_env_evar sigma env =
-  let nc' = nf_named_context_evar sigma (Environ.named_context env) in
-  let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
-    push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
-
-let nf_evar_info evc info = map_evar_info (nf_evar evc) info
-
-let nf_evar_map evm =
-  Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
-
-let nf_evar_map_undefined evm =
-  Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm
-
-(*-------------------*)
-(* Auxiliary functions for the conversion algorithms modulo evars
- *)
-
-(* A probably faster though more approximative variant of
-   [has_undefined (nf_evar c)]: instances are not substituted and
-   maybe an evar occurs in an instance and it would disappear by
-   instantiation *)
-
-let has_undefined_evars evd t =
-  let rec has_ev t =
-    match kind_of_term t with
-    | Evar (ev,args) ->
-        (match evar_body (Evd.find evd ev) with
-        | Evar_defined c ->
-            has_ev c; Array.iter has_ev args
-        | Evar_empty ->
-	    raise NotInstantiatedEvar)
-    | _ -> iter_constr has_ev t in
-  try let _ = has_ev t in false
-  with (Not_found | NotInstantiatedEvar) -> true
-
-let is_ground_term evd t =
-  not (has_undefined_evars evd t)
-
-let is_ground_env evd env =
-  let open Context.Rel.Declaration in
-  let is_ground_rel_decl = function
-    | LocalDef (_,b,_) -> is_ground_term evd b
-    | _ -> true in
-  let open Context.Named.Declaration in
-  let is_ground_named_decl = function
-    | LocalDef (_,b,_) -> is_ground_term evd b
-    | _ -> true in
-  List.for_all is_ground_rel_decl (rel_context env) &&
-  List.for_all is_ground_named_decl (named_context env)
-
-(* Memoization is safe since evar_map and environ are applicative
-   structures *)
-let memo f =
-  let m = ref None in
-  fun x y -> match !m with
-  | Some (x', y', r) when x == x' && y == y' -> r
-  | _ -> let r = f x y in m := Some (x, y, r); r
-
-let is_ground_env = memo is_ground_env
-
-(* Return the head evar if any *)
-
-exception NoHeadEvar
-
-let head_evar =
-  let rec hrec c = match kind_of_term c with
-    | Evar (evk,_)   -> evk
-    | Case (_,_,c,_) -> hrec c
-    | App (c,_)      -> hrec c
-    | Cast (c,_,_)   -> hrec c
-    | _              -> raise NoHeadEvar
-  in
-  hrec
-
-(* Expand head evar if any (currently consider only applications but I
-   guess it should consider Case too) *)
-
-let whd_head_evar_stack sigma c =
-  let rec whrec (c, l as s) =
-    match kind_of_term c with
-      | Evar (evk,args as ev) ->
-        let v =
-          try Some (existential_value sigma ev)
-          with NotInstantiatedEvar | Not_found  -> None in
-        begin match v with
-        | None -> s
-        | Some c -> whrec (c, l)
-        end
-      | Cast (c,_,_) -> whrec (c, l)
-      | App (f,args) -> whrec (f, args :: l)
-      | _ -> s
-  in
-  whrec (c, [])
-
-let whd_head_evar sigma c =
-  let (f, args) = whd_head_evar_stack sigma c in
-  (** optim: don't reallocate if empty/singleton *)
-  match args with
-  | [] -> f
-  | [arg] -> mkApp (f, arg)
-  | _ -> mkApp (f, Array.concat args)
-
-(**********************)
-(* Creating new metas *)
-(**********************)
-
-let meta_counter_summary_name = "meta counter"
-
-(* Generator of metavariables *)
-let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
-  fun () -> incr meta_ctr; !meta_ctr
-
-let mk_new_meta () = mkMeta(new_meta())
-
-(* The list of non-instantiated existential declarations (order is important) *)
-
-let non_instantiated sigma =
-  let listev = Evd.undefined_map sigma in
-  Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev
-
-(************************)
-(* Manipulating filters *)
-(************************)
-
-let make_pure_subst evi args =
-  let open Context.Named.Declaration in
-  snd (List.fold_right
-    (fun decl (args,l) ->
-      match args with
-        | a::rest -> (rest, (get_id decl, a)::l)
-        | _ -> anomaly (Pp.str "Instance does not match its signature"))
-    (evar_filtered_context evi) (Array.rev_to_list args,[]))
-
-(*------------------------------------*
- * functional operations on evar sets *
- *------------------------------------*)
-
-(* [push_rel_context_to_named_context] builds the defining context and the
- * initial instance of an evar. If the evar is to be used in context
- *
- * Gamma =  a1     ...    an xp      ...       x1
- *          \- named part -/ \- de Bruijn part -/
- *
- * then the x1...xp are turned into variables so that the evar is declared in
- * context
- *
- *          a1     ...    an xp      ...       x1
- *          \----------- named part ------------/
- *
- * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
- * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
- * in context Gamma.
- *
- * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
- * Remark 2: If some of the ai or xj are definitions, we keep them in the
- *   instance. This is necessary so that no unfolding of local definitions
- *   happens when inferring implicit arguments (consider e.g. the problem
- *   "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
- *   produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
- *   the hole to be instantiated by x', not by x (which would have been
- *   the case in [invert_definition] if x' had disappeared from the instance).
- *   Note that at any time, if, in some context env, the instance of
- *   declaration x:A is t and the instance of definition x':=phi(x) is u, then
- *   we have the property that u and phi(t) are convertible in env.
- *)
-
-let subst2 subst vsubst c =
-  substl subst (replace_vars vsubst c)
-
-let push_rel_context_to_named_context env typ =
-  (* compute the instances relative to the named context and rel_context *)
-  let open Context.Named.Declaration in
-  let ids = List.map get_id (named_context env) in
-  let inst_vars = List.map mkVar ids in
-  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
-  let replace_var_named_declaration id0 id decl =
-    let id' = get_id decl in
-    let id' = if Id.equal id0 id' then id else id' in
-    let vsubst = [id0 , mkVar id] in
-    decl |> set_id id' |> map_constr (replace_vars vsubst)
-  in
-  let replace_var_named_context id0 id  env =
-    let nc = Environ.named_context env in
-    let nc' = List.map (replace_var_named_declaration id0 id) nc in
-    Environ.reset_with_named_context (val_of_named_context nc') env
-  in
-  let extract_if_neq id = function
-    | Anonymous -> None
-    | Name id' when id_ord id id' = 0 -> None
-    | Name id' -> Some id'
-  in
-  (* move the rel context to a named context and extend the named instance *)
-  (* with vars of the rel context *)
-  (* We do keep the instances corresponding to local definition (see above) *)
-  let (subst, vsubst, _, env) =
-    Context.Rel.fold_outside
-      (fun decl (subst, vsubst, avoid, env) ->
-        let open Context.Rel.Declaration in
-        let na = get_name decl in
-	let c = get_value decl in
-	let t = get_type decl in
-        let open Context.Named.Declaration in
-        let id =
-          (* ppedrot: we want to infer nicer names for the refine tactic, but
-             keeping at the same time backward compatibility in other code
-             using this function. For now, we only attempt to preserve the
-             old behaviour of Program, but ultimately, one should do something
-             about this whole name generation problem. *)
-          if Flags.is_program_mode () then next_name_away na avoid
-          else next_ident_away (id_of_name_using_hdchar env t na) avoid
-        in
-        match extract_if_neq id na with
-        | Some id0 when not (is_section_variable id0) ->
-            (* spiwack: if [id<>id0], rather than introducing a new
-               binding named [id], we will keep [id0] (the name given
-               by the user) and rename [id0] into [id] in the named
-               context. Unless [id] is a section variable. *)
-            let subst = List.map (replace_vars [id0,mkVar id]) subst in
-            let vsubst = (id0,mkVar id)::vsubst in
-            let d = match c with
-              | None -> LocalAssum (id0, subst2 subst vsubst t)
-              | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-            let env = replace_var_named_context id0  id env in
-            (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
-        | _ ->
-            (* spiwack: if [id0] is a section variable renaming it is
-               incorrect. We revert to a less robust behaviour where
-               the new binder has name [id]. Which amounts to the same
-               behaviour than when [id=id0]. *)
-            let d = match c with
-              | None -> LocalAssum (id, subst2 subst vsubst t)
-              | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-	    (mkVar id :: subst, vsubst, id::avoid, push_named d env)
-      )
-      (rel_context env) ~init:([], [], ids, env) in
-  (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
-
-(*------------------------------------*
- * Entry points to define new evars   *
- *------------------------------------*)
-
-let default_source = (Loc.ghost,Evar_kinds.InternalHole)
-
-let restrict_evar evd evk filter candidates =
-  let evd = Sigma.to_evar_map evd in
-  let evd, evk' = Evd.restrict evk filter ?candidates evd in
-  Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
-
-let new_pure_evar_full evd evi =
-  let evd = Sigma.to_evar_map evd in
-  let (evd, evk) = Evd.new_evar evd evi in
-  let evd = Evd.declare_future_goal evk evd in
-  Sigma.Unsafe.of_pair (evk, evd)
-
-let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
-  let evd = Sigma.to_evar_map evd in
-  let default_naming = Misctypes.IntroAnonymous in
-  let naming = Option.default default_naming naming in
-  let evi = {
-    evar_hyps = sign;
-    evar_concl = typ;
-    evar_body = Evar_empty;
-    evar_filter = filter;
-    evar_source = src;
-    evar_candidates = candidates;
-    evar_extra = store; }
-  in
-  let (evd, newevk) = Evd.new_evar evd ~naming evi in
-  let evd =
-    if principal then Evd.declare_principal_goal newevk evd
-    else Evd.declare_future_goal newevk evd
-  in
-  Sigma.Unsafe.of_pair (newevk, evd)
-
-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 Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  Sigma (mkEvar (newevk,Array.of_list instance), evd, p)
-
-(* [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 ?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 ?principal instance
-
-let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  (Sigma.to_evar_map evd, evk)
-
-let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
-  let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
-  let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
-  Sigma ((e, s), evd', p +> q)
-
-let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
-  let sigma = Sigma.Unsafe.of_evar_map !evdref in
-  let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in
-  let sigma = Sigma.to_evar_map sigma in
-    evdref := sigma;
-    c
-
-let new_Type ?(rigid=Evd.univ_flexible) env evd = 
-  let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
-  Sigma (mkSort s, sigma, p)
-
-let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
-  let evd', s = new_sort_variable rigid !evdref in
-    evdref := evd'; mkSort s
-
-  (* The same using side-effect *)
-let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
-  let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
-  evdref := evd';
-  ev
-
-(* This assumes an evar with identity instance and generalizes it over only
-   the De Bruijn part of the context *)
-let generalize_evar_over_rels sigma (ev,args) =
-  let evi = Evd.find sigma ev in
-  let sign = named_context_of_val evi.evar_hyps in
-  List.fold_left2
-    (fun (c,inst as x) a d ->
-      if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
-     (evi.evar_concl,[]) (Array.to_list args) sign
-
-(************************************)
-(* Removing a dependency in an evar *)
-(************************************)
-
-type clear_dependency_error =
-| OccurHypInSimpleClause of Id.t option
-| EvarTypingBreak of existential
-
-exception ClearDependencyError of Id.t * clear_dependency_error
-
-let cleared = Store.field ()
-
-exception Depends of Id.t
-
-let rec check_and_clear_in_constr env evdref err ids c =
-  (* returns a new constr where all the evars have been 'cleaned'
-     (ie the hypotheses ids have been removed from the contexts of
-     evars) *)
-  let check id' =
-    if Id.Set.mem id' ids then
-      raise (ClearDependencyError (id',err))
-  in
-    match kind_of_term c with
-      | Var id' ->
-	  check id'; c
-
-      | ( Const _ | Ind _ | Construct _ ) ->
-          let vars = Environ.vars_of_global env c in
-            Id.Set.iter check vars; c
-
-      | Evar (evk,l as ev) ->
-	  if Evd.is_defined !evdref evk then
-	    (* If evk is already defined we replace it by its definition *)
-	    let nc = whd_evar !evdref c in
-	      (check_and_clear_in_constr env evdref err ids nc)
-	  else
-	    (* We check for dependencies to elements of ids in the
-	       evar_info corresponding to e and in the instance of
-	       arguments. Concurrently, we build a new evar
-	       corresponding to e where hypotheses of ids have been
-	       removed *)
-	    let evi = Evd.find_undefined !evdref evk in
-	    let ctxt = Evd.evar_filtered_context evi in
-	    let (rids,filter) =
-              List.fold_right2
-                (fun h a (ri,filter) ->
-                  try
-                  (* Check if some id to clear occurs in the instance
-                     a of rid in ev and remember the dependency *)
-                    let check id = if Id.Set.mem id ids then raise (Depends id) in
-                    let () = Id.Set.iter check (collect_vars a) in
-                  (* Check if some rid to clear in the context of ev
-                     has dependencies in another hyp of the context of ev
-                     and transitively remember the dependency *)
-                    let check id _ =
-                      if occur_var_in_decl (Global.env ()) id h
-                      then raise (Depends id)
-                    in
-                    let () = Id.Map.iter check ri in
-                  (* No dependency at all, we can keep this ev's context hyp *)
-                    (ri, true::filter)
-                  with Depends id -> let open Context.Named.Declaration in
-                                     (Id.Map.add (get_id h) id ri, false::filter))
-		ctxt (Array.to_list l) (Id.Map.empty,[]) in
-	    (* Check if some rid to clear in the context of ev has dependencies
-	       in the type of ev and adjust the source of the dependency *)
-	    let _nconcl =
-	      try
-                let nids = Id.Map.domain rids in
-                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi)
-	      with ClearDependencyError (rid,err) ->
-		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
-
-            if Id.Map.is_empty rids then c
-            else
-              let origfilter = Evd.evar_filter evi in
-              let filter = Evd.Filter.apply_subfilter origfilter filter in
-              let evd = Sigma.Unsafe.of_evar_map !evdref in
-              let Sigma (_, evd, _) = restrict_evar evd evk filter None in
-              let evd = Sigma.to_evar_map evd in
-              evdref := evd;
-	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
-	      let evi = Evd.find !evdref evk in
-	      let extra = evi.evar_extra in
-	      let extra' = Store.set extra cleared true in
-	      let evi' = { evi with evar_extra = extra' } in
-	      evdref := Evd.add !evdref evk evi' ;
-	    (* spiwack: /hacking session *)
-              whd_evar !evdref c
-
-      | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
-
-let clear_hyps_in_evi_main env evdref hyps terms ids =
-  (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
-     hypothesis does not depend on a element of ids, and erases ids in
-     the contexts of the evars occurring in evi *)
-  let terms =
-    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
-  let nhyps =
-    let open Context.Named.Declaration in
-    let check_context decl =
-      let err = OccurHypInSimpleClause (Some (get_id decl)) in
-      map_constr (check_and_clear_in_constr env evdref err ids) decl
-    in
-    let check_value vk = match force_lazy_val vk with
-    | None -> vk
-    | Some (_, d) ->
-      if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
-        (* v does depend on any of ids, it's ok *)
-        vk
-      else
-        (* v depends on one of the cleared hyps:
-            we forget the computed value *)
-        dummy_lazy_val ()
-    in
-      remove_hyps ids check_context check_value hyps
-  in
-  (nhyps,terms)
-
-let clear_hyps_in_evi env evdref hyps concl ids =
-  match clear_hyps_in_evi_main env evdref hyps [concl] ids with
-  | (nhyps,[nconcl]) -> (nhyps,nconcl)
-  | _ -> assert false
-
-let clear_hyps2_in_evi env evdref hyps t concl ids =
-  match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with
-  | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
-  | _ -> assert false
-
-(* spiwack: a few functions to gather evars on which goals depend. *)
-let queue_set q is_dependent set =
-  Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
-let queue_term q is_dependent c =
-  queue_set q is_dependent (evars_of_term c)
-
-let process_dependent_evar q acc evm is_dependent e =
-  let evi = Evd.find evm e in
-  (* Queues evars appearing in the types of the goal (conclusion, then
-     hypotheses), they are all dependent. *)
-  queue_term q true evi.evar_concl;
-  List.iter begin fun decl ->
-    let open Context.Named.Declaration in
-    queue_term q true (get_type decl);
-    match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,b,_) -> queue_term q true b
-  end (Environ.named_context_of_val evi.evar_hyps);
-  match evi.evar_body with
-  | Evar_empty ->
-      if is_dependent then Evar.Map.add e None acc else acc
-  | Evar_defined b ->
-      let subevars = evars_of_term b in
-      (* evars appearing in the definition of an evar [e] are marked
-         as dependent when [e] is dependent itself: if [e] is a
-         non-dependent goal, then, unless they are reach from another
-         path, these evars are just other non-dependent goals. *)
-      queue_set q is_dependent subevars;
-      if is_dependent then Evar.Map.add e (Some subevars) acc else acc
-
-let gather_dependent_evars q evm =
-  let acc = ref Evar.Map.empty in
-  while not (Queue.is_empty q) do
-    let (is_dependent,e) = Queue.pop q in
-    (* checks if [e] has already been added to [!acc] *)
-    begin if not (Evar.Map.mem e !acc) then
-        acc := process_dependent_evar q !acc evm is_dependent e  
-    end
-  done;
-  !acc
-
-let gather_dependent_evars evm l =
-  let q = Queue.create () in
-  List.iter (fun a -> Queue.add (false,a) q) l;
-  gather_dependent_evars q evm
-
-(* /spiwack *)
-
-(** The following functions return the set of undefined evars
-    contained in the object, the defined evars being traversed.
-    This is roughly a combination of the previous functions and
-    [nf_evar]. *)
-
-let undefined_evars_of_term evd t =
-  let rec evrec acc c =
-    match kind_of_term c with
-      | Evar (n, l) ->
-	let acc = Array.fold_left evrec acc l in
-	(try match (Evd.find evd n).evar_body with
-	  | Evar_empty -> Evar.Set.add n acc
-	  | Evar_defined c -> evrec acc c
-	 with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
-      | _ -> fold_constr evrec acc c
-  in
-  evrec Evar.Set.empty t
-
-let undefined_evars_of_named_context evd nc =
-  let open Context.Named.Declaration in
-  Context.Named.fold_outside
-    (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
-    nc
-    ~init:Evar.Set.empty
-
-let undefined_evars_of_evar_info evd evi =
-  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
-    (Evar.Set.union
-       (match evi.evar_body with
-	 | Evar_empty -> Evar.Set.empty
-	 | Evar_defined b -> undefined_evars_of_term evd b)
-       (undefined_evars_of_named_context evd
-	  (named_context_of_val evi.evar_hyps)))
-
-(* spiwack: this is a more complete version of
-   {!Termops.occur_evar}. The latter does not look recursively into an
-   [evar_map]. If unification only need to check superficially, tactics
-   do not have this luxury, and need the more complete version. *)
-let occur_evar_upto sigma n c =
-  let rec occur_rec c = match kind_of_term c with
-    | Evar (sp,_) when Evar.equal sp n -> raise Occur
-    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
-    | _ -> iter_constr occur_rec c
-  in
-  try occur_rec c; false with Occur -> true
-
-(* We don't try to guess in which sort the type should be defined, since
-   any type has type Type. May cause some trouble, but not so far... *)
-
-let judge_of_new_Type evd =
-  let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
-  Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
-
-let subterm_source evk (loc,k) =
-  let evk = match k with
-    | Evar_kinds.SubEvar (evk) -> evk
-    | _ -> evk in
-  (loc,Evar_kinds.SubEvar evk)
-
-
-(** Term exploration up to instantiation. *)
-let kind_of_term_upto sigma t =
-  Constr.kind (whd_evar sigma t)
-
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
-    [u] up to existential variable instantiation and equalisable
-    universes. The term [t] is interpreted in [sigma1] while [u] is
-    interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extention of those in [sigma1]. *)
-let eq_constr_univs_test sigma1 sigma2 t u =
-  (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
-  let open Evd in
-  let fold cstr sigma =
-    try Some (add_universe_constraints sigma cstr)
-    with Univ.UniverseInconsistency _ | UniversesDiffer -> None
-  in
-  let ans =
-    Universes.eq_constr_univs_infer_with
-      (fun t -> kind_of_term_upto sigma1 t)
-      (fun u -> kind_of_term_upto sigma2 u)
-      (universes sigma2) fold t u sigma2
-  in
-  match ans with None -> false | Some _ -> true
-
-type type_constraint = types option
-type val_constraint = constr option
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
deleted file mode 100644
index ffff2c5dd..000000000
--- a/pretyping/evarutil.mli
+++ /dev/null
@@ -1,221 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Evd
-open Environ
-
-(** {5 This modules provides useful functions for unification modulo evars } *)
-
-(** {6 Metas} *)
-
-(** [new_meta] is a generator of unique meta variables *)
-val new_meta : unit -> metavariable
-val mk_new_meta : unit -> constr
-
-(** {6 Creating a fresh evar given their type and context} *)
-val new_evar :
-  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> (constr, 'r) Sigma.sigma
-
-val new_pure_evar :
-  named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> (evar, 'r) Sigma.sigma
-
-val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
-
-(** the same with side-effects *)
-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 ->
-  ?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 -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  (constr * sorts, 'r) Sigma.sigma
-
-val e_new_type_evar : env -> evar_map ref ->
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
-
-val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
-
-val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  constr list option -> (existential_key, 'r) Sigma.sigma
-
-(** Polymorphic constants *)
-
-val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
-val e_new_global : evar_map ref -> Globnames.global_reference -> constr
-
-(** Create a fresh evar in a context different from its definition context:
-   [new_evar_instance sign evd ty inst] creates a new evar of context
-   [sign] and type [ty], [inst] is a mapping of the evar context to
-   the context where the evar should occur. This means that the terms
-   of [inst] are typed in the occurrence context and their type (seen
-   as a telescope) is [sign] *)
-val new_evar_instance :
- named_context_val -> 'r Sigma.t -> 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 -> (constr, 'r) Sigma.sigma
-
-val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
-
-val safe_evar_value : evar_map -> existential -> constr option
-
-(** {6 Evars/Metas switching...} *)
-
-val non_instantiated : evar_map -> evar_info Evar.Map.t
-
-(** {6 Unification utils} *)
-
-(** [head_evar c] returns the head evar of [c] if any *)
-exception NoHeadEvar
-val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
-
-(* Expand head evar if any *)
-val whd_head_evar :  evar_map -> constr -> constr
-
-(* An over-approximation of [has_undefined (nf_evars evd c)] *)
-val has_undefined_evars : evar_map -> constr -> bool
-
-val is_ground_term :  evar_map -> constr -> bool
-val is_ground_env  :  evar_map -> env -> bool
-
-(** [gather_dependent_evars evm seeds] classifies the evars in [evm]
-    as dependent_evars and goals (these may overlap). A goal is an
-    evar in [seeds] or an evar appearing in the (partial) definition
-    of a goal. A dependent evar is an evar appearing in the type
-    (hypotheses and conclusion) of a goal, or in the type or (partial)
-    definition of a dependent evar.  The value return is a map
-    associating to each dependent evar [None] if it has no (partial)
-    definition or [Some s] if [s] is the list of evars appearing in
-    its (partial) definition. *)
-val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
-
-(** The following functions return the set of undefined evars
-    contained in the object, the defined evars being traversed.
-    This is roughly a combination of the previous functions and
-    [nf_evar]. *)
-
-val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
-val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
-val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
-
-(** [occur_evar_upto sigma k c] returns [true] if [k] appears in
-    [c]. It looks up recursively in [sigma] for the value of existential
-    variables. *)
-val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
-
-(** {6 Value/Type constraints} *)
-
-val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
-
-(***********************************************************)
-
-(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
-    uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
-
-val whd_evar :  evar_map -> constr -> constr
-val nf_evar :  evar_map -> constr -> constr
-val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar :
-   evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
-   evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
-   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-
-val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
-val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
-val nf_env_evar : evar_map -> env -> env
-
-val nf_evar_info : evar_map -> evar_info -> evar_info
-val nf_evar_map : evar_map -> evar_map
-val nf_evar_map_undefined : evar_map -> evar_map
-
-(** Presenting terms without solved evars *)
-
-val nf_evars_universes : evar_map -> constr -> constr
-
-val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr)
-val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst
-
-(** Normalize the evar map w.r.t. universes, after simplification of constraints.
-    Return the substitution function for constrs as well. *)
-val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
-
-(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
-exception Uninstantiated_evar of existential_key
-val flush_and_check_evars :  evar_map -> constr -> constr
-
-(** {6 Term manipulation up to instantiation} *)
-
-(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
-    as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
-    value of [e] in [sigma] is (recursively) used. *)
-val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
-
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
-    [u] up to existential variable instantiation and equalisable
-    universes. The term [t] is interpreted in [sigma1] while [u] is
-    interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extention of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
-
-(** {6 Removing hyps in evars'context}
-raise OccurHypInSimpleClause if the removal breaks dependencies *)
-
-type clear_dependency_error =
-| OccurHypInSimpleClause of Id.t option
-| EvarTypingBreak of existential
-
-exception ClearDependencyError of Id.t * clear_dependency_error
-
-(* spiwack: marks an evar that has been "defined" by clear.
-    used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
-val cleared : bool Store.field
-
-val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
-  Id.Set.t -> named_context_val * types
-
-val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
-  Id.Set.t -> named_context_val * types * types
-
-val push_rel_context_to_named_context : Environ.env -> types ->
-  named_context_val * types * constr list * constr list * (identifier*constr) list
-
-val generalize_evar_over_rels : evar_map -> existential -> types * constr list
-
-(** Evar combinators *)
-
-val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
-val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
-val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-
-val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
-  Evar_kinds.t Loc.located
-
-val meta_counter_summary_name : string
-
-(** Deprecater *)
-
-type type_constraint = types option
-type val_constraint = constr option
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index be517d1aa..c8b3307d7 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,6 +1,5 @@
 Locusops
 Pretype_errors
-Evarutil
 Reductionops
 Inductiveops
 Vnorm
@@ -21,7 +20,6 @@ Patternops
 Constr_matching
 Tacred
 Typeclasses_errors
-Proofview
 Typeclasses
 Classops
 Program
diff --git a/pretyping/proofview.ml b/pretyping/proofview.ml
deleted file mode 100644
index ba664cafa..000000000
--- a/pretyping/proofview.ml
+++ /dev/null
@@ -1,1211 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-
-(** This files defines the basic mechanism of proofs: the [proofview]
-    type is the state which tactics manipulate (a global state for
-    existential variables, together with the list of goals), and the type
-    ['a tactic] is the (abstract) type of tactics modifying the proof
-    state and returning a value of type ['a]. *)
-
-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
-
-(** Returns a stylised view of a proofview for use by, for instance,
-    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. *)
-(* In this version: returns the list of focused goals together with
-   the [evar_map] context. *)
-let proofview p =
-  p.comb , p.solution
-
-let compact el ({ solution } as pv) =
-  let nf = Evarutil.nf_evar solution 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
-  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
-  msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
-  new_el, { pv with solution = new_solution; }
-
-
-(** {6 Starting and querying a proof view} *)
-
-type telescope =
-  | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
-
-let typeclass_resolvable = Evd.Store.field ()
-
-let dependent_init =
-  (* Goals are created with a store which marks them as unresolvable
-     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
-  (* 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 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 = [] }
-  in
-  fun t ->
-    let entry, v = aux t in
-    (* The created goal are not to be shelved. *)
-    let solution = Evd.reset_future_goals v.solution in
-    entry, { v with solution }
-
-let init =
-  let rec aux sigma = function
-    | [] -> TNil sigma
-    | (env,g)::l -> TCons (env,sigma,g,(fun sigma _ -> aux sigma l))
-  in
-  fun sigma l -> dependent_init (aux sigma l)
-
-let initial_goals initial = initial
-
-let finished = function
-  | {comb = []} -> true
-  | _  -> false
-
-let return { solution=defs } = defs
-
-let return_constr { solution = defs } c = Evarutil.nf_evar defs c
-
-let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry)
-
-
-(** {6 Focusing commands} *)
-
-(** A [focus_context] represents the part of the proof view which has
-    been removed by a focusing action, it can be used to unfocus later
-    on. *)
-(* 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
-
-
-(** Returns a stylised view of a focus_context for use by, for
-    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. *)
-(* In this version: the goals in the context, as a "zipper" (the first
-   list is in reversed order). *)
-let focus_context f = f
-
-(** 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
-    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 <
-    i]. *)
-let focus_sublist i j l =
-  let (left,sub_right) = CList.goto (i-1) l in
-  let (sub, right) = 
-    try CList.chop (j-i+1) sub_right
-    with Failure _ -> raise CList.IndexOutOfRange
-  in
-  (sub, (left,right))
-
-(** Inverse operation to the previous one. *)
-let unfocus_sublist (left,right) s =
-  CList.rev_append left (s@right)
-
-
-(** [focus i j] focuses a proofview on the goals from index [i] to
-    index [j] (inclusive, goals are indexed from [1]). I.e. goals
-    number [i] to [j] become the only focused goals of the returned
-    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 )
-
-
-(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
-    the current avatar of [g] (for instance [g] was changed by [clear]
-    into [g']). It returns [None] if [g] has been (partially)
-    solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
-   behaviour of its definition may depend sensitively to the actual
-   definition of [Evd.find]. Currently, [Evd.find] starts looking for
-   a value in the heap of undefined variable, which is small. Hence in
-   the most common case, where [advance] is applied to an unsolved
-   goal ([advance] is used to figure if a side effect has modified the
-   goal) it terminates quickly. *)
-let rec advance sigma g =
-  let open Evd in
-  let evi = Evd.find sigma g in
-  match evi.evar_body with
-  | Evar_empty -> Some g
-  | Evar_defined v ->
-      if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then
-        let (e,_) = Term.destEvar v in
-        advance sigma e
-      else
-        None
-
-(** [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 (advance defs) l
-
-(** Unfocuses a proofview with respect to a context. *)
-let unfocus c sp =
-  { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
-
-
-(** {6 The tactic monad} *)
-
-(** - Tactics are objects which apply a transformation to all the
-    subgoals of the current view at the same time. By opposition to
-    the old vision of applying it to a single goal. It allows tactics
-    such as [shelve_unifiable], tactics to reorder the focused goals,
-    or global automation tactic for dependent subgoals (instantiating
-    an evar has influences on the other goals of the proof in
-    progress, not being able to take that into account causes the
-    current eauto tactic to fail on some instances where it could
-    succeed).  Another benefit is that it is possible to write tactics
-    that can be executed even if there are no focused goals.
-    - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seen as a function (without argument) which returns a value of
-    type 'a and modifies the environment (in our case: the view).
-    Tactics of course have arguments, but these are given at the
-    meta-level as OCaml functions.  Most tactics in the sense we are
-    used to return [()], that is no really interesting values. But
-    some might pass information around.  The tactics seen in Coq's
-    Ltac are (for now at least) only [unit tactic], the return values
-    are kept for the OCaml toolkit.  The operation or the monad are
-    [Proofview.tclUNIT] (which is the "return" of the tactic monad)
-    [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN]
-    (which is a specialized bind on unit-returning tactics).
-    - Tactics have support for full-backtracking. Tactics can be seen
-    having multiple success: if after returning the first success a
-    failure is encountered, the tactic can backtrack and use a second
-    success if available. The state is backtracked to its previous
-    value, except the non-logical state defined in the {!NonLogical}
-    module below.
-*)
-(* spiwack: as far as I'm aware this doesn't really relate to
-   F. Kirchner and C. Muñoz. *)
-
-module Proof = Logical
-
-(** type of tactics:
-
-   tactics can
-   - access the environment,
-   - report unsafe status, shelved goals and given up goals
-   - access and change the current [proofview]
-   - backtrack on previous changes of the proofview *)
-type +'a tactic = 'a Proof.t
-
-(** Applies a tactic to the current proofview. *)
-let apply env t sp =
-  let open Logic_monad in
-  let ans = Proof.repr (Proof.run t false (sp,env)) in
-  let ans = Logic_monad.NonLogical.run ans in
-  match ans with
-  | Nil (e, info) -> iraise (TacticFailure e, info)
-  | Cons ((r, (state, _), status, info), _) ->
-    let (status, gaveup) = status in
-    let status = (status, state.shelf, gaveup) in
-    let state = { state with shelf = [] } in
-    r, state, status, Trace.to_tree info
-
-
-
-(** {7 Monadic primitives} *)
-
-(** Unit of the tactic monad. *)
-let tclUNIT = Proof.return
-
-(** Bind operation of the tactic monad. *)
-let tclBIND = Proof.(>>=)
-
-(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation,
-    it's a specialized "bind". *)
-let tclTHEN = Proof.(>>)
-
-(** [tclIGNORE t] has the same operational content as [t], but drops
-    the returned value. *)
-let tclIGNORE = Proof.ignore
-
-module Monad = Proof
-
-
-
-(** {7 Failure and backtracking} *)
-
-
-(** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO ?info e =
-  let info = match info with
-  | None -> Exninfo.null
-  | Some info -> info
-  in
-  Proof.zero (e, info)
-
-(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
-    the successes of [t1] have been depleted and it failed with [e],
-    then it behaves as [t2 e]. In other words, [tclOR] inserts a
-    backtracking point. *)
-let tclOR = Proof.plus
-
-(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
-    success or [t2 e] if [t1] fails with [e]. It is analogous to
-    [try/with] handler of exception in that it is not a backtracking
-    point. *)
-let tclORELSE t1 t2 =
-  let open Logic_monad in
-  let open Proof in
-  split t1 >>= function
-    | Nil e -> t2 e
-    | Cons (a,t1') -> plus (return a) t1'
-
-(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
-    succeeds at least once then it behaves as [tclBIND a s] otherwise,
-    if [a] fails with [e], then it behaves as [f e]. *)
-let tclIFCATCH a s f =
-  let open Logic_monad in
-  let open Proof in
-  split a >>= function
-    | Nil e -> f e
-    | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
-
-(** [tclONCE t] behave like [t] except it has at most one success:
-    [tclONCE t] stops after the first success of [t]. If [t] fails
-    with [e], [tclONCE t] also fails with [e]. *)
-let tclONCE = Proof.once
-
-exception MoreThanOneSuccess
-let _ = Errors.register_handler begin function
-  | MoreThanOneSuccess -> Errors.error "This tactic has more than one success."
-  | _ -> raise Errors.Unhandled
-end
-
-(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
-    success. Otherwise it fails. The tactic [t] is run until its first
-    success, then a failure with exception [e] is simulated. It [t]
-    yields another success, then [tclEXACTLY_ONCE e t] fails with
-    [MoreThanOneSuccess] (it is a user error). Otherwise,
-    [tclEXACTLY_ONCE e t] succeeds with the first success of
-    [t]. Notice that the choice of [e] is relevant, as the presence of
-    further successes may depend on [e] (see {!tclOR}). *)
-let tclEXACTLY_ONCE e t =
-  let open Logic_monad in
-  let open Proof in
-  split t >>= function
-    | Nil (e, info) -> tclZERO ~info e
-    | Cons (x,k) ->
-        Proof.split (k (e, Exninfo.null)) >>= function
-          | Nil _ -> tclUNIT x
-          | _ -> tclZERO MoreThanOneSuccess
-
-
-(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
-type 'a case =
-| Fail of iexn
-| Next of 'a * (iexn -> 'a tactic)
-let tclCASE t =
-  let open Logic_monad in
-  let map = function
-  | Nil e -> Fail e
-  | Cons (x, t) -> Next (x, t)
-  in
-  Proof.map map (Proof.split t)
-
-let tclBREAK = Proof.break
-
-
-
-(** {7 Focusing tactics} *)
-
-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 set_nosuchgoals_hook f = nosuchgoals_hook := f
-
-
-
-(* This uses the hook above *)
-let _ = Errors.register_handler begin function
-  | NoSuchGoals n ->
-    let suffix = !nosuchgoals_hook n in
-    Errors.errorlabstrm ""
-      (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix)
-  | _ -> raise Errors.Unhandled
-end
-
-(** [tclFOCUS_gen 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 open Proof in
-  Pv.get >>= fun initial ->
-  try
-    let (focused,context) = focus i j initial in
-    Pv.set focused >>
-    t >>= fun result ->
-    Pv.modify (fun next -> unfocus context next) >>
-    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
-
-(** Like {!tclFOCUS} but selects a single goal by name. *)
-let tclFOCUSID id t =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  try
-    let ev = Evd.evar_key id initial.solution in
-    try
-      let n = CList.index Evar.equal ev initial.comb in
-      (* goal is already under focus *)
-      let (focused,context) = focus n n initial in
-      Pv.set focused >>
-        t >>= fun result ->
-      Pv.modify (fun next -> unfocus context next) >>
-        return result
-    with Not_found ->
-      (* otherwise, save current focus and work purely on the shelve *)
-      Comb.set [ev] >>
-        t >>= fun result ->
-      Comb.set initial.comb  >>
-        return result
-  with Not_found -> tclZERO (NoSuchGoals 1)
-
-(** {7 Dispatching on goals} *)
-
-exception SizeMismatch of int*int
-let _ = Errors.register_handler begin function
-  | SizeMismatch (i,_) ->
-      let open Pp in
-      let errmsg =
-        str"Incorrect number of goals" ++ spc() ++
-        str"(expected "++int i++str(String.plural i " tactic") ++ str")."
-      in
-      Errors.errorlabstrm "" errmsg
-  | _ -> raise Errors.Unhandled
-end
-
-(** A variant of [Monad.List.iter] where we iter over the focused list
-    of goals. The argument tactic is executed in a focus comprising
-    only of the current goal, a goal which has been solved by side
-    effect is skipped. The generated subgoals are concatenated in
-    order.  *)
-let iter_goal i =
-  let open Proof in
-  Comb.get >>= fun initial ->
-  Proof.List.fold_left begin fun (subgoals as cur) goal ->
-    Solution.get >>= fun step ->
-    match advance step goal with
-    | None -> return cur
-    | Some goal ->
-        Comb.set [goal] >>
-        i goal >>
-        Proof.map (fun comb -> comb :: subgoals) Comb.get
-  end [] initial >>= fun subgoals ->
-  Solution.get >>= fun evd ->
-  Comb.set CList.(undefined evd (flatten (rev subgoals)))
-
-(** 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
-    by side effect is skipped. The generated subgoals are concatenated
-    in order. *)
-let fold_left2_goal i s l =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  let err =
-    return () >>= fun () -> (* Delay the computation of list lengths. *)
-    tclZERO (SizeMismatch (CList.length initial.comb,CList.length l))
-  in 
-  Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
-    Solution.get >>= fun step ->
-    match advance step goal with
-    | None -> return cur
-    | Some goal ->
-        Comb.set [goal] >>
-        i goal a r >>= fun r ->
-        Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get
-  end (s,[]) initial.comb l >>= fun (r,subgoals) ->
-  Solution.get >>= fun evd ->
-  Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
-  return r
-
-(** Dispatch tacticals are used to apply a different tactic to each
-    goal under focus. They come in two flavours: [tclDISPATCH] takes a
-    list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL]
-    takes a list of ['a tactic] and returns an ['a list tactic].
-
-    They both work by applying each of the tactic in a focus
-    restricted to the corresponding goal (starting with the first
-    goal). In the case of [tclDISPATCHL], the tactic returns a list of
-    the same size as the argument list (of tactics), each element
-    being the result of the tactic executed in the corresponding goal.
-
-    When the length of the tactic list is not the number of goal,
-    raises [SizeMismatch (g,t)] where [g] is the number of available
-    goals, and [t] the number of tactics passed.
-
-    [tclDISPATCHGEN join tacs] generalises both functions as the
-    successive results of [tacs] are stored in reverse order in a
-    list, and [join] is used to convert the result into the expected
-    form. *)
-let tclDISPATCHGEN0 join tacs =
-  match tacs with
-  | [] ->
-      begin 
-        let open Proof in
-        Comb.get >>= function
-        | [] -> tclUNIT (join [])
-        | comb -> tclZERO (SizeMismatch (CList.length comb,0))
-      end
-  | [tac] ->
-      begin
-        let open Proof in
-        Pv.get >>= function
-        | { comb=[goal] ; solution } ->
-            begin match advance solution goal with
-            | None -> tclUNIT (join [])
-            | Some _ -> Proof.map (fun res -> join [res]) tac
-            end
-        | {comb} -> tclZERO (SizeMismatch(CList.length comb,1))
-      end
-  | _ ->
-      let iter _ t cur = Proof.map (fun y -> y :: cur) t in
-      let ans = fold_left2_goal iter [] tacs in
-      Proof.map join ans
-
-let tclDISPATCHGEN join tacs =
-  let branch t = InfoL.tag (Info.DBranch) t in
-  let tacs = CList.map branch tacs in
-  InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
-
-let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs
-
-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]. *)
-let extend_to_list startxs rx endxs l =
-  (* spiwack: I use [l] essentially as a natural number *)
-  let rec duplicate acc = function
-    | [] -> acc
-    | _::rest -> duplicate (rx::acc) rest
-  in
-  let rec tail to_match rest =
-    match rest, to_match with
-    | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
-    | _::rest , _::to_match -> tail to_match rest
-    | _ , [] -> duplicate endxs rest
-  in
-  let rec copy pref rest =
-    match rest,pref with
-    | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
-    | _::rest, a::pref -> a::(copy pref rest)
-    | _ , [] -> tail endxs rest
-  in
-  copy startxs l
-
-(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r]
-    tactic is "repeated" enough time such that every goal has a tactic
-    assigned to it ([b] is the list of tactics applied to the first
-    goals, [e] to the last goals, and [r] is applied to every goal in
-    between). *)
-let tclEXTEND tacs1 rtac tacs2 =
-  let open Proof in
-  Comb.get >>= fun comb ->
-  try
-    let tacs = extend_to_list tacs1 rtac tacs2 comb in
-    tclDISPATCH tacs
-  with SizeMismatch _ ->
-    tclZERO (SizeMismatch(
-      CList.length comb,
-      (CList.length tacs1)+(CList.length tacs2)))
-(* spiwack: failure occurs only when the number of goals is too
-   small. Hence we can assume that [rtac] is replicated 0 times for
-   any error message. *)
-
-(** [tclEXTEND [] tac []]. *)
-let tclINDEPENDENT tac =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  match initial.comb with
-  | [] -> tclUNIT ()
-  | [_] -> tac
-  | _ ->
-      let tac = InfoL.tag (Info.DBranch) tac in
-      InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
-
-
-
-(** {7 Goal manipulation} *)
-
-(** Shelves all the goals under focus. *)
-let shelve =
-  let open Proof in
-  Comb.get >>= fun initial ->
-  Comb.set [] >>
-  InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
-  Shelf.modify (fun gls -> gls @ initial)
-
-
-(** [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
-
-(** [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 sigma g l =
-  CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) 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
-
-(** Shelves the unifiable goals under focus, i.e. the goals which
-    appear in other goals under focus (the unfocused goals are not
-    considered). *)
-let shelve_unifiable =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  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)
-
-(** [guard_no_unifiable] returns the list of unifiable goals if some
-    goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
-let guard_no_unifiable =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  let (u,n) = partition_unifiable initial.solution initial.comb in
-  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 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 =
-  (* advance the goals in case of clear *)
-  let l = undefined p.solution l in
-  { p with comb = p.comb@l }
-
-let with_shelf tac =
-  let open Proof in
-  Pv.get >>= fun pv ->
-  let { shelf; solution } = pv in
-  Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >>
-  tac >>= fun ans ->
-  Pv.get >>= fun npv ->
-  let { shelf = gls; solution = sigma } = npv in
-  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
-  Pv.set { npv with shelf; solution = sigma } >>
-  tclUNIT (CList.rev_append gls' gls, ans)
-
-(** [goodmod p m] computes the representative of [p] modulo [m] in the
-    interval [[0,m-1]].*)
-let goodmod p m =
-  let p' = p mod m in
-  (* if [n] is negative [n mod l] is negative of absolute value less
-     than [l], so [(n mod l)+l] is the representative of [n] in the
-     interval [[0,l-1]].*)
-  if p' < 0 then p'+m else p'
-
-let cycle n =
-  let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
-  Comb.modify begin fun initial ->
-    let l = CList.length initial in
-    let n' = goodmod n l in
-    let (front,rear) = CList.chop n' initial in
-    rear@front
-  end
-
-let swap i j =
-  let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
-  Comb.modify begin fun initial ->
-    let l = CList.length initial in
-    let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
-    let i = goodmod i l and j = goodmod j l in
-    CList.map_i begin fun k x ->
-      match k with
-      | k when Int.equal k i -> CList.nth initial j
-      | k when Int.equal k j -> CList.nth initial i
-      | _ -> x
-    end 0 initial
-  end
-
-let revgoals =
-  let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >>
-  Comb.modify CList.rev
-
-let numgoals =
-  let open Proof in
-  Comb.get >>= fun comb ->
-  return (CList.length comb)
-
-
-
-(** {7 Access primitives} *)
-
-let tclEVARMAP = Solution.get
-
-let tclENV = Env.get
-
-
-
-(** {7 Put-like primitives} *)
-
-
-let emit_side_effects eff x =
-  { x with solution = Evd.emit_side_effects eff x.solution }
-
-let tclEFFECTS eff =
-  let open Proof in
-  return () >>= fun () -> (* The Global.env should be taken at exec time *)
-  Env.set (Global.env ()) >>
-  Pv.modify (fun initial -> emit_side_effects eff initial)
-
-let mark_as_unsafe = Status.put false
-
-(** Gives up on the goal under focus. Reports an unsafe status. Proofs
-    with given up goals cannot be closed. *)
-let give_up =
-  let open Proof in
-  Comb.get >>= fun initial ->
-  Comb.set [] >>
-  mark_as_unsafe >>
-  InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
-  Giveup.put initial
-
-
-
-(** {7 Control primitives} *)
-
-
-module Progress = struct
-
-  let eq_constr = Evarutil.eq_constr_univs_test
-
-  (** equality function on hypothesis contexts *)
-  let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
-    let open Environ in
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
-    let eq_named_declaration d1 d2 =
-      match d1, d2 with
-      | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
-         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
-      | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
-         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
-         && eq_constr sigma1 sigma2 t1 t2
-      | _ ->
-         false
-    in List.equal eq_named_declaration c1 c2
-
-  let eq_evar_body sigma1 sigma2 b1 b2 =
-    let open Evd in
-    match b1, b2 with
-    | Evar_empty, Evar_empty -> true
-    | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2
-    | _ -> false
-
-  let eq_evar_info sigma1 sigma2 ei1 ei2 =
-    let open Evd in
-    eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl &&
-    eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) &&
-    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
-
-end
-
-let tclPROGRESS t =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  t >>= fun res ->
-  Pv.get >>= fun final ->
-  (* [*_test] test absence of progress. [quick_test] is approximate
-     whereas [exhaustive_test] is complete. *)
-  let quick_test =
-    initial.solution == final.solution && initial.comb == final.comb
-  in
-  let exhaustive_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 (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
-
-exception Timeout
-let _ = Errors.register_handler begin function
-  | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
-  | _ -> Pervasives.raise Errors.Unhandled
-end
-
-let tclTIMEOUT n t =
-  let open Proof in
-  (* spiwack: as one of the monad is a continuation passing monad, it
-     doesn't force the computation to be threaded inside the underlying
-     (IO) monad. Hence I force it myself by asking for the evaluation of
-     a dummy value first, lest [timeout] be called when everything has
-     already been computed. *)
-  let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in
-  Proof.get >>= fun initial ->
-  Proof.current >>= fun envvar ->
-  Proof.lift begin
-    Logic_monad.NonLogical.catch
-      begin
-        let open Logic_monad.NonLogical in
-        timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
-        match r with
-        | Logic_monad.Nil e -> return (Util.Inr e)
-        | Logic_monad.Cons (r, _) -> return (Util.Inl r)
-      end
-      begin let open Logic_monad.NonLogical in function (e, info) ->
-        match e with
-        | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
-        | Logic_monad.TacticFailure e ->
-          return (Util.Inr (e, info))
-        | e -> Logic_monad.NonLogical.raise ~info e
-      end
-  end >>= function
-    | Util.Inl (res,s,m,i) ->
-        Proof.set s >>
-        Proof.put m >>
-        Proof.update (fun _ -> i) >>
-        return res
-    | Util.Inr (e, info) -> tclZERO ~info e
-
-let tclTIME s t =
-  let pr_time t1 t2 n msg =
-    let msg =
-      if n = 0 then
-        str msg
-      else
-        str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking")
-    in
-    msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
-             System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in
-  let rec aux n t =
-    let open Proof in
-    tclUNIT () >>= fun () ->
-    let tstart = System.get_time() in
-    Proof.split t >>= let open Logic_monad in function
-    | Nil (e, info) ->
-      begin
-        let tend = System.get_time() in
-        pr_time tstart tend n "failure";
-        tclZERO ~info e
-      end
-    | Cons (x,k) ->
-        let tend = System.get_time() in
-        pr_time tstart tend n "success";
-        tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
-  in aux 0 t
-
-
-
-(** {7 Unsafe primitives} *)
-
-module Unsafe = struct
-
-  let tclEVARS evd =
-    Pv.modify (fun ps -> { ps with solution = evd })
-
-  let tclNEWGOALS gls =
-    Pv.modify begin fun step ->
-      let gls = undefined step.solution gls in
-      { step with comb = step.comb @ gls }
-    end
-
-  let tclGETGOALS = Comb.get
-
-  let tclSETGOALS = Comb.set
-
-  let tclEVARSADVANCE evd =
-    Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
-
-  let tclEVARUNIVCONTEXT ctx = 
-    Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
-
-  let reset_future_goals p =
-    { p with solution = Evd.reset_future_goals p.solution }
-
-  let mark_as_goal evd content =
-    let info = Evd.find evd content in
-    let info =
-      { info with Evd.evar_source = match info.Evd.evar_source with
-      | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
-      | loc,_ -> loc,Evar_kinds.GoalEvar }
-    in
-    let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
-    | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
-    | Some () -> info
-    in
-    Evd.add evd content info
-
-  let advance = advance
-
-  let typeclass_resolvable = typeclass_resolvable
-
-end
-
-module UnsafeRepr = Proof.Unsafe
-
-let (>>=) = tclBIND
-let (<*>) = tclTHEN
-let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-
-(** {6 Goal-dependent tactics} *)
-
-let goal_env evars gl =
-  let evi = Evd.find evars gl in
-  Evd.evar_filtered_env evi
-
-let goal_nf_evar sigma gl =
-  let evi = Evd.find sigma gl in
-  let evi = Evarutil.nf_evar_info sigma evi in
-  let sigma = Evd.add sigma gl evi in
-  (gl, sigma)
-
-let goal_extra evars gl =
-  let evi = Evd.find evars gl in
-  evi.Evd.evar_extra
-
-
-let catchable_exception = function
-  | Logic_monad.Exception _ -> false
-  | e -> Errors.noncritical e
-
-
-module Goal = struct
-
-  type ('a, 'r) t = {
-    env : Environ.env;
-    sigma : Evd.evar_map;
-    concl : Term.constr ;
-    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 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 raw_concl { concl=concl } = concl
-
-
-  let gmake_with info env sigma goal = 
-    { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
-      sigma = sigma ;
-      concl = Evd.evar_concl info ;
-      self = goal }
-
-  let nf_gmake env sigma goal =
-    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
-
-  let nf_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
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl))
-      with e when catchable_exception e ->
-        let (e, info) = Errors.push e in
-        tclZERO ~info e
-    end
-    end
-
-  let normalize { self } =
-    Env.get >>= fun env ->
-    tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = nf_gmake env sigma self in
-    tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
-  let gmake env sigma goal =
-    let info = Evd.find sigma goal in
-    gmake_with info env sigma goal
-
-  let enter f =
-    let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in
-    InfoL.tag (Info.Dispatch) begin
-    iter_goal begin fun goal ->
-      Env.get >>= fun env ->
-      tclEVARMAP >>= fun sigma ->
-      try f (gmake env sigma goal)
-      with e when catchable_exception e ->
-        let (e, info) = Errors.push e in
-        tclZERO ~info e
-    end
-    end
-
-  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) = Errors.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) = Errors.push e in
-        tclZERO ~info e
-    end
-    end
-
-  let goals =
-    Pv.get >>= fun step ->
-    let sigma = step.solution in
-    let map goal =
-      match advance sigma goal with
-      | None -> None (** ppedrot: Is this check really necessary? *)
-      | Some goal ->
-        let gl =
-          Env.get >>= fun env ->
-          tclEVARMAP >>= fun sigma ->
-          tclUNIT (gmake env sigma goal)
-        in
-        Some gl
-    in
-    tclUNIT (CList.map_filter map step.comb)
-
-  (* compatibility *)
-  let goal { self=self } = self
-
-  let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t)
-
-end
-
-
-
-(** {6 Trace} *)
-
-module Trace = struct
-
-  let record_info_trace = InfoL.record_trace
-
-  let log m = InfoL.leaf (Info.Msg m)
-  let name_tactic m t = InfoL.tag (Info.Tactic m) t
-
-  let pr_info ?(lvl=0) info =
-    assert (lvl >= 0);
-    Info.(print (collapse lvl info))
-
-end
-
-
-
-(** {6 Non-logical state} *)
-
-module NonLogical = Logic_monad.NonLogical
-
-let tclLIFT = Proof.lift
-
-let tclCHECKINTERRUPT =
-   tclLIFT (NonLogical.make Control.check_for_interrupt)
-
-
-
-
-
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 = struct
-  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-
-  let tactic 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 glsigma  =
-          tac { Evd.it = gl ; sigma = evd; }  in
-        let sigma = glsigma.Evd.sigma in
-        let g = 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
-      in
-      let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
-      let sgs = CList.flatten goalss in
-      let sgs = undefined evd sgs in
-      InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
-      Pv.set { ps with solution = evd; comb = sgs; }
-    with e when catchable_exception e ->
-      let (e, info) = Errors.push e in
-      tclZERO ~info e
-
-
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  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; }
-    end
-      
-  let has_unresolved_evar pv =
-    Evd.has_undefined pv.solution
-
-  (* Main function in the implementation of Grab Existential Variables.*)
-  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 }
-      
-    
-
-  (* 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 }
-
-  let top_goals initial { solution=solution; } =
-    let goals = CList.map (fun (t,_) -> fst (Term.destEvar 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)
-    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 (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
-      { Evd.sigma = final.solution ; it = final.comb }
-    with Logic_monad.TacticFailure e as src ->
-      let (_, info) = Errors.push src in
-      iraise (e, info)
-
-  let put_status = Status.put
-
-  let catchable_exception = catchable_exception
-
-  let wrap_exceptions f =
-    try f ()
-    with e when catchable_exception e ->
-      let (e, info) = Errors.push e in tclZERO ~info e
-
-end
-
-(** {7 Notations} *)
-
-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
diff --git a/pretyping/proofview.mli b/pretyping/proofview.mli
deleted file mode 100644
index 7996b7969..000000000
--- a/pretyping/proofview.mli
+++ /dev/null
@@ -1,589 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This files defines the basic mechanism of proofs: the [proofview]
-    type is the state which tactics manipulate (a global state for
-    existential variables, together with the list of goals), and the type
-    ['a tactic] is the (abstract) type of tactics modifying the proof
-    state and returning a value of type ['a]. *)
-
-open Util
-open Term
-
-(** Main state of tactics *)
-type proofview
-
-(** Returns a stylised view of a proofview for use by, for instance,
-    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. *)
-(* In this version: returns the list of focused goals together with
-   the [evar_map] context. *)
-val proofview : proofview -> Goal.goal list * Evd.evar_map
-
-
-(** {6 Starting and querying a proof view} *)
-
-(** Abstract representation of the initial goals of a proof. *)
-type entry
-
-(** Optimize memory consumption *)
-val compact : entry -> proofview -> entry * proofview
-
-(** Initialises a proofview, the main argument is a list of
-    environments (including a [named_context] which are used as
-    hypotheses) pair with conclusion types, creating accordingly many
-    initial goals. Because a proof does not necessarily starts in an
-    empty [evar_map] (indeed a proof can be triggered by an incomplete
-    pretyping), [init] takes an additional argument to represent the
-    initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
-
-(** A [telescope] is a list of environment and conclusion like in
-    {!init}, except that each element may depend on the previous
-    goals. The telescope passes the goals in the form of a
-    [Term.constr] which represents the goal as an [evar]. The
-    [evar_map] is threaded in state passing style. *)
-type telescope =
-  | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
-
-(** Like {!init}, but goals are allowed to be dependent on one
-    another. Dependencies between goals is represented with the type
-    [telescope] instead of [list]. Note that the first [evar_map] of
-    the telescope plays the role of the [evar_map] argument in
-    [init]. *)
-val dependent_init  : telescope -> entry * proofview
-
-(** [finished pv] is [true] if and only if [pv] is complete. That is,
-    if it has an empty list of focused goals. There could still be
-    unsolved subgoaled, but they would then be out of focus. *)
-val finished : proofview -> bool
-
-(** Returns the current [evar] state. *)
-val return : proofview -> Evd.evar_map
-
-val partial_proof : entry -> proofview -> constr list
-val initial_goals : entry -> (constr * types) list
-
-
-
-(** {6 Focusing commands} *)
-
-(** A [focus_context] represents the part of the proof view which has
-    been removed by a focusing action, it can be used to unfocus later
-    on. *)
-type focus_context
-
-(** Returns a stylised view of a focus_context for use by, for
-    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. *)
-(* In this version: the goals in the context, as a "zipper" (the first
-   list is in reversed order). *)
-val focus_context : focus_context -> Goal.goal list * Goal.goal list
-
-(** [focus i j] focuses a proofview on the goals from index [i] to
-    index [j] (inclusive, goals are indexed from [1]). I.e. goals
-    number [i] to [j] become the only focused goals of the returned
-    proofview.  It returns the focused proofview, and a context for
-    the focus stack. *)
-val focus : int -> int -> proofview -> proofview * focus_context
-
-(** Unfocuses a proofview with respect to a context. *)
-val unfocus : focus_context -> proofview -> proofview
-
-
-(** {6 The tactic monad} *)
-
-(** - Tactics are objects which apply a transformation to all the
-    subgoals of the current view at the same time. By opposition to
-    the old vision of applying it to a single goal. It allows tactics
-    such as [shelve_unifiable], tactics to reorder the focused goals,
-    or global automation tactic for dependent subgoals (instantiating
-    an evar has influences on the other goals of the proof in
-    progress, not being able to take that into account causes the
-    current eauto tactic to fail on some instances where it could
-    succeed).  Another benefit is that it is possible to write tactics
-    that can be executed even if there are no focused goals.
-    - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seen as a function (without argument) which returns a value of
-    type 'a and modifies the environment (in our case: the view).
-    Tactics of course have arguments, but these are given at the
-    meta-level as OCaml functions.  Most tactics in the sense we are
-    used to return [()], that is no really interesting values. But
-    some might pass information around.  The tactics seen in Coq's
-    Ltac are (for now at least) only [unit tactic], the return values
-    are kept for the OCaml toolkit.  The operation or the monad are
-    [Proofview.tclUNIT] (which is the "return" of the tactic monad)
-    [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN]
-    (which is a specialized bind on unit-returning tactics).
-    - Tactics have support for full-backtracking. Tactics can be seen
-    having multiple success: if after returning the first success a
-    failure is encountered, the tactic can backtrack and use a second
-    success if available. The state is backtracked to its previous
-    value, except the non-logical state defined in the {!NonLogical}
-    module below.
-*)
-
-
-(** The abstract type of tactics *)
-type +'a tactic 
-
-(** Applies a tactic to the current proofview. Returns a tuple
-    [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv]
-    is the updated proofview, [b] a boolean which is [true] if the
-    tactic has not done any action considered unsafe (such as
-    admitting a lemma), [sh] is the list of goals which have been
-    shelved by the tactic, and [gu] the list of goals on which the
-    tactic has given up. In case of multiple success the first one is
-    selected. If there is no success, fails with
-    {!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
-                                                   * proofview
-                                                   * (bool*Goal.goal list*Goal.goal list)
-                                                   * Proofview_monad.Info.tree
-
-(** {7 Monadic primitives} *)
-
-(** Unit of the tactic monad. *)
-val tclUNIT : 'a -> 'a tactic
- 
-(** Bind operation of the tactic monad. *)
-val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-
-(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
-    it's a specialized "bind". *)
-val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
-
-(** [tclIGNORE t] has the same operational content as [t], but drops
-    the returned value. *)
-val tclIGNORE : 'a tactic -> unit tactic
-
-(** Generic monadic combinators for tactics. *)
-module Monad : Monad.S with type +'a t = 'a tactic
-
-(** {7 Failure and backtracking} *)
-
-(** [tclZERO e] fails with exception [e]. It has no success. *)
-val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
-
-(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
-    the successes of [t1] have been depleted and it failed with [e],
-    then it behaves as [t2 e]. In other words, [tclOR] inserts a
-    backtracking point. *)
-val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
-
-(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
-    success or [t2 e] if [t1] fails with [e]. It is analogous to
-    [try/with] handler of exception in that it is not a backtracking
-    point. *)
-val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
-
-(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
-    succeeds at least once then it behaves as [tclBIND a s] otherwise,
-    if [a] fails with [e], then it behaves as [f e]. *)
-val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic
-
-(** [tclONCE t] behave like [t] except it has at most one success:
-    [tclONCE t] stops after the first success of [t]. If [t] fails
-    with [e], [tclONCE t] also fails with [e]. *)
-val tclONCE : 'a tactic -> 'a tactic
-
-(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
-    success. Otherwise it fails. The tactic [t] is run until its first
-    success, then a failure with exception [e] is simulated. It [t]
-    yields another success, then [tclEXACTLY_ONCE e t] fails with
-    [MoreThanOneSuccess] (it is a user error). Otherwise,
-    [tclEXACTLY_ONCE e t] succeeds with the first success of
-    [t]. Notice that the choice of [e] is relevant, as the presence of
-    further successes may depend on [e] (see {!tclOR}). *)
-exception MoreThanOneSuccess
-val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
-
-(** [tclCASE t] splits [t] into its first success and a
-    continuation. It is the most general primitive to control
-    backtracking. *)
-type 'a case =
-  | Fail of iexn
-  | Next of 'a * (iexn -> 'a tactic)
-val tclCASE : 'a tactic -> 'a case tactic
-
-(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
-    stopping after the first success, it succeeds like [t] until a
-    failure with an exception [e] such that [p e = Some e'] is raised. At
-    which point it drops the remaining successes, failing with [e'].
-    [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *)
-val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
-
-
-(** {7 Focusing tactics} *)
-
-(** [tclFOCUS i j t] applies [t] after focusing on the goals number
-    [i] to [j] (see {!focus}). The rest of the goals is restored after
-    the tactic action. If the specified range doesn't correspond to
-    existing goals, fails with [NoSuchGoals] (a user error). this
-    exception is caught at toplevel with a default message + a hook
-    message that can be customized by [set_nosuchgoals_hook] below.
-    This hook is used to add a suggestion about bullets when
-    applicable. *)
-exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit
-
-val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
-
-(** [tclFOCUSID x t] applies [t] on a (single) focused goal like
-    {!tclFOCUS}. The goal is found by its name rather than its
-    number.*)
-val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic
-
-(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the
-    specified range doesn't correspond to existing goals, behaves like
-    [tclUNIT ()] instead of failing. *)
-val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic
-
-
-(** {7 Dispatching on goals} *)
-
-(** Dispatch tacticals are used to apply a different tactic to each
-    goal under focus. They come in two flavours: [tclDISPATCH] takes a
-    list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL]
-    takes a list of ['a tactic] and returns an ['a list tactic].
-
-    They both work by applying each of the tactic in a focus
-    restricted to the corresponding goal (starting with the first
-    goal). In the case of [tclDISPATCHL], the tactic returns a list of
-    the same size as the argument list (of tactics), each element
-    being the result of the tactic executed in the corresponding goal.
-
-    When the length of the tactic list is not the number of goal,
-    raises [SizeMismatch (g,t)] where [g] is the number of available
-    goals, and [t] the number of tactics passed. *)
-exception SizeMismatch of int*int
-val tclDISPATCH : unit tactic list -> unit tactic
-val tclDISPATCHL : 'a tactic list -> 'a list tactic
-
-(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r]
-    tactic is "repeated" enough time such that every goal has a tactic
-    assigned to it ([b] is the list of tactics applied to the first
-    goals, [e] to the last goals, and [r] is applied to every goal in
-    between). *)
-val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
-
-(** [tclINDEPENDENT tac] runs [tac] on each goal successively, from
-    the first one to the last one. Backtracking in one goal is
-    independent of backtracking in another. It is equivalent to
-    [tclEXTEND [] tac []]. *)
-val tclINDEPENDENT : unit tactic -> unit tactic
-
-
-(** {7 Goal manipulation} *)
-
-(** Shelves all the goals under focus. The goals are placed on the
-    shelf for later use (or being solved by side-effects). *)
-val shelve : unit tactic
-
-(** Shelves the unifiable goals under focus, i.e. the goals which
-    appear in other goals under focus (the unfocused goals are not
-    considered). *)
-val shelve_unifiable : unit tactic
-
-(** [guard_no_unifiable] returns the list of unifiable goals if some
-    goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
-val guard_no_unifiable : Names.Name.t list option tactic
-
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
-    goals of p *)
-val unshelve : Goal.goal list -> proofview -> proofview
-
-(** [with_shelf tac] executes [tac] and returns its result together with the set
-    of goals shelved by [tac]. The current shelf is unchanged. *)
-val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
-
-(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
-    is negative, then it puts the [n] last goals first.*)
-val cycle : int -> unit tactic
-
-(** [swap i j] swaps the position of goals number [i] and [j]
-    (negative numbers can be used to address goals from the end. Goals
-    are indexed from [1]. For simplicity index [0] corresponds to goal
-    [1] as well, rather than raising an error. *)
-val swap : int -> int -> unit tactic
-
-(** [revgoals] reverses the list of focused goals. *)
-val revgoals : unit tactic
-
-(** [numgoals] returns the number of goals under focus. *)
-val numgoals : int tactic
-
-
-(** {7 Access primitives} *)
-
-(** [tclEVARMAP] doesn't affect the proof, it returns the current
-    [evar_map]. *)
-val tclEVARMAP : Evd.evar_map tactic
-
-(** [tclENV] doesn't affect the proof, it returns the current
-    environment. It is not the environment of a particular goal,
-    rather the "global" environment of the proof. The goal-wise
-    environment is obtained via {!Proofview.Goal.env}. *)
-val tclENV : Environ.env tactic
-
-
-(** {7 Put-like primitives} *)
-
-(** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Safe_typing.private_constants -> unit tactic
-
-(** [mark_as_unsafe] declares the current tactic is unsafe. *)
-val mark_as_unsafe : unit tactic
-
-(** Gives up on the goal under focus. Reports an unsafe status. Proofs
-    with given up goals cannot be closed. *)
-val give_up : unit tactic
-
-
-(** {7 Control primitives} *)
-
-(** [tclPROGRESS t] checks the state of the proof after [t]. It it is
-    identical to the state before, then [tclePROGRESS t] fails, otherwise
-    it succeeds like [t]. *)
-val tclPROGRESS : 'a tactic -> 'a tactic
-
-(** Checks for interrupts *)
-val tclCHECKINTERRUPT : unit tactic
-
-exception Timeout
-(** [tclTIMEOUT n t] can have only one success.
-    In case of timeout if fails with [tclZERO Timeout]. *)
-val tclTIMEOUT : int -> 'a tactic -> 'a tactic
-
-(** [tclTIME s t] displays time for each atomic call to t, using s as an
-    identifying annotation if present *)
-val tclTIME : string option -> 'a tactic -> 'a tactic
-
-(** {7 Unsafe primitives} *)
-
-(** The primitives in the [Unsafe] module should be avoided as much as
-    possible, since they can make the proof state inconsistent. They are
-    nevertheless helpful, in particular when interfacing the pretyping and
-    the proof engine. *)
-module Unsafe : sig
-
-  (** [tclEVARS sigma] replaces the current [evar_map] by [sigma]. If
-      [sigma] has new unresolved [evar]-s they will not appear as
-      goal. If goals have been solved in [sigma] they will still
-      appear as unsolved goals. *)
-  val tclEVARS : Evd.evar_map -> unit tactic
-    
-  (** Like {!tclEVARS} but also checks whether goals have been solved. *)
-  val tclEVARSADVANCE : Evd.evar_map -> unit tactic
-
-  (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
-      being proved, appending them to the list of focused goals. If a
-      goal is already solved, it is not added. *)
-  val tclNEWGOALS : Goal.goal list -> unit tactic
-
-  (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
-      goal is already solved, it is not set. *)
-  val tclSETGOALS : Goal.goal list -> unit tactic
-
-  (** [tclGETGOALS] returns the list of goals under focus. *)
-  val tclGETGOALS : Goal.goal list tactic
-
-  (** Sets the evar universe context. *)
-  val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
-
-  (** Clears the future goals store in the proof view. *)
-  val reset_future_goals : proofview -> proofview
-
-  (** Give an evar the status of a goal (changes its source location
-      and makes it unresolvable for type classes. *)
-  val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
-
-  (** [advance sigma g] returns [Some g'] if [g'] is undefined and is
-      the current avatar of [g] (for instance [g] was changed by [clear]
-      into [g']). It returns [None] if [g] has been (partially)
-      solved. *)
-  val advance : Evd.evar_map -> Evar.t -> Evar.t option
-
-  val typeclass_resolvable : unit Evd.Store.field
-
-end
-
-(** This module gives access to the innards of the monad. Its use is
-    restricted to very specific cases. *)
-module UnsafeRepr :
-sig
-  type state = Proofview_monad.Logical.Unsafe.state
-  val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t
-  val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic
-end
-
-(** {6 Goal-dependent tactics} *)
-
-module Goal : sig
-
-  (** Type of goals.
-
-      The first parameter type is a phantom argument indicating whether the data
-      contained in the goal has been normalized w.r.t. the current sigma. If it
-      is the case, it is flagged [ `NF ]. You may still access the un-normalized
-      data using {!assume} if you known you do not rely on the assumption of
-      being normalized, at your own risk.
-
-      The second parameter is a stage indicating where the goal belongs. See
-      module {!Sigma}.
-  *)
-  type ('a, 'r) t
-
-  (** Assume that you do not need the goal to be normalized. *)
-  val assume : ('a, 'r) t -> ([ `NF ], 'r) t
-
-  (** Normalises the argument goal. *)
-  val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic
-
-  (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
-      respectively the conclusion of [gl], the hypotheses of [gl], the
-      environment of [gl] (i.e. the global environment and the
-      hypotheses) and the current evar map. *)
-  val concl : ([ `NF ], 'r) t -> Term.constr
-  val hyps : ([ `NF ], 'r) t -> Context.Named.t
-  val env : ('a, 'r) t -> Environ.env
-  val sigma : ('a, 'r) t -> 'r Sigma.t
-  val extra : ('a, 'r) t -> Evd.Store.t
-
-  (** Returns the goal's conclusion even if the goal is not
-      normalised. *)
-  val raw_concl : ('a, 'r) t -> Term.constr
-
-  type ('a, 'b) enter =
-    { enter : 'r. ('a, 'r) t -> 'b }
-
-  (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
-      independently, in the manner of {!tclINDEPENDENT} except that
-      the current goal is also given as an argument to [t]. The goal
-      is normalised with respect to evars. *)
-  val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic
-
-  (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
-  val enter : ([ `LZ ], unit tactic) enter -> unit tactic
-
-  type ('a, 'b) s_enter =
-    { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
-
-  (** A variant of {!enter} allows to work with a monotonic state. The evarmap
-      returned by the argument is put back into the current state before firing
-      the returned tactic. *)
-  val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic
-
-  (** Like {!s_enter}, but normalizes the goal beforehand. *)
-  val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic
-
-  (** Recover the list of current goals under focus, without evar-normalization.
-      FIXME: encapsulate the level in an existential type. *)
-  val goals : ([ `LZ ], 'r) t tactic list tactic
-
-  (** Compatibility: avoid if possible *)
-  val goal : ([ `NF ], 'r) t -> Evar.t
-
-  (** Every goal is valid at a later stage. FIXME: take a later evarmap *)
-  val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t
-
-end
-
-
-(** {6 Trace} *)
-
-module Trace : sig
-
-  (** [record_info_trace t] behaves like [t] except the [info] trace
-      is stored. *)
-  val record_info_trace : 'a tactic -> 'a tactic
-
-  val log : Proofview_monad.lazy_msg -> unit tactic
-  val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
-
-  val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds
-
-end
-
-
-(** {6 Non-logical state} *)
-
-(** The [NonLogical] module allows the execution of effects (including
-    I/O) in tactics (non-logical side-effects are not discarded at
-    failures). *)
-module NonLogical : module type of Logic_monad.NonLogical
-
-(** [tclLIFT c] is a tactic which behaves exactly as [c]. *)
-val tclLIFT : 'a NonLogical.t -> 'a tactic
-
-
-(**/**)
-
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 : sig
-  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-  val tactic : tac -> unit tactic
-
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  val nf_evar_goals : unit tactic
-
-  val has_unresolved_evar : proofview -> bool
-
-  (* Main function in the implementation of Grab Existential Variables.
-     Resets the proofview's goals so that it contains all unresolved evars
-     (in chronological order of insertion). *)
-  val grab : proofview -> proofview
-
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  val goals : proofview -> Evar.t list Evd.sigma
-
-  val top_goals : entry -> proofview -> Evar.t list Evd.sigma
-  
-  (* returns the existential variable used to start the proof *)
-  val top_evars : entry -> Evd.evar list
-
-  (* Caution: this function loses quite a bit of information. It
-     should be avoided as much as possible.  It should work as
-     expected for a tactic obtained from {!V82.tactic} though. *)
-  val of_tactic : 'a tactic -> tac
-
-  (* marks as unsafe if the argument is [false] *)
-  val put_status : bool -> unit tactic
-
-  (* exception for which it is deemed to be safe to transmute into
-     tactic failure. *)
-  val catchable_exception : exn -> bool
-
-  (* transforms every Ocaml (catchable) exception into a failure in
-     the monad. *)
-  val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
-end
-
-(** {7 Notations} *)
-
-module Notations : sig
-
-  (** {!tclBIND} *)
-  val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-  (** {!tclTHEN} *)
-  val (<*>) : unit tactic -> 'a tactic -> 'a tactic
-  (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
-  val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
-
-  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