1 files changed, 4 insertions, 12 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 639f48e77..fdb0a215d 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -45,9 +45,9 @@ let compact el ({ solution } as pv) =
   let pruned_solution = Evd.drop_all_defined solution in
   let apply_subst_einfo _ ei =
     Evd.({ ei with
-       evar_concl =  nf0 ei.evar_concl;
+       evar_concl =  nf ei.evar_concl;
        evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
-       evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in
+       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
   Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
@@ -875,8 +875,7 @@ module Progress = struct
 
   (** 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 c1 = EConstr.named_context_of_val ctx1 and c2 = EConstr.named_context_of_val ctx2 in
     let eq_named_declaration d1 d2 =
       match d1, d2 with
       | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
@@ -1086,8 +1085,6 @@ module Goal = struct
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  let assume (gl : t) = (gl : t)
-
   let print { sigma; self } = { Evd.it = self; sigma }
 
   let state { state=state } = state
@@ -1101,7 +1098,7 @@ module Goal = struct
   let gmake_with info env sigma goal state =
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
       sigma = sigma ;
-      concl = EConstr.of_constr (Evd.evar_concl info);
+      concl = Evd.evar_concl info;
       state = state ;
       self = goal }
 
@@ -1275,11 +1272,6 @@ module V82 = struct
       
     
 
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  let goals { comb = comb ; solution = solution; } =
-   { Evd.it = List.map drop_state comb ; sigma = solution }
-
   let top_goals initial { solution=solution; } =
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }