From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 proofs/refine.ml | 51 +++++++++++++++++++--------------------------------
 1 file changed, 19 insertions(+), 32 deletions(-)

(limited to 'proofs/refine.ml')

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 909556b1..198e057e 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
 module NamedDecl = Context.Named.Declaration
 
 let extract_prefix env info =
-  let ctx1 = List.rev (Environ.named_context env) in
+  let ctx1 = List.rev (EConstr.named_context env) in
   let ctx2 = List.rev (Evd.evar_context info) in
   let rec share l1 l2 accu = match l1, l2 with
   | d1 :: l1, d2 :: l2 ->
@@ -29,47 +29,34 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = EConstr.of_constr (NamedDecl.get_type decl) in
-    let evdref = ref sigma in
-    let _ = Typing.e_sort_of env evdref t in
-    let () = match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
+    let t = NamedDecl.get_type decl in
+    let sigma, _ = Typing.sort_of env sigma t in
+    let sigma = match decl with
+    | LocalAssum _ -> sigma
+    | LocalDef (_,body,_) -> Typing.check env sigma body t
     in
-    (!evdref, Environ.push_named decl env)
+    (sigma, EConstr.push_named decl env)
   in
   let (common, changed) = extract_prefix env info in
-  let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+  let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
-  let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
-  !evdref
-
-let typecheck_proof c concl env sigma =
-  let evdref = ref sigma in
-  let () = Typing.e_check env evdref c concl in
-  !evdref
+  let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
+  sigma
 
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
 (* Get the side-effect's constant declarations to update the monad's
   * environmnent *)
-let add_if_undefined kn cb env =
-  try ignore(Environ.lookup_constant kn env); env
-  with Not_found -> Environ.add_constant kn cb env
+let add_if_undefined env eff =
+  let open Entries in
+  try ignore(Environ.lookup_constant eff.seff_constant env); env
+  with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
 
 (* Add the side effects to the monad's environment, if not already done. *)
-let add_side_effect env = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-    add_if_undefined kn cb env
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-    List.fold_left (fun env (_,kn,cb,eff_env) ->
-        add_if_undefined kn cb env) env l
-
-let add_side_effects env effects =
-  List.fold_left (fun env eff -> add_side_effect env eff) env effects
+let add_side_effects env eff =
+  List.fold_left add_if_undefined env eff
 
 let generic_refine ~typecheck f gl =
   let sigma = Proofview.Goal.sigma gl in
@@ -93,7 +80,7 @@ let generic_refine ~typecheck f gl =
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
+  let sigma = if typecheck then Typing.check env sigma c concl else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
@@ -106,7 +93,6 @@ let generic_refine ~typecheck f gl =
   let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
   let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
   (** Proceed to the refinement *)
-  let c = EConstr.Unsafe.to_constr c in
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
     (** Nothing to do, the goal has been solved by side-effect *)
@@ -124,7 +110,8 @@ let generic_refine ~typecheck f gl =
   (** Mark goals *)
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
-  let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
+  let trace () = Pp.(hov 2 (str"simple refine"++spc()++
+                            Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
-- 
cgit v1.2.3