1 files changed, 97 insertions, 38 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6d7dcb9257..a382e9873f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -16,6 +16,8 @@
 open Pp
 open Util
 open Proofview_monad
+open Sigma.Notations
+open Context.Named.Declaration
 
 (** Main state of tactics *)
 type proofview = Proofview_monad.proofview
@@ -64,7 +66,9 @@ let dependent_init =
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
+    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
@@ -350,7 +354,7 @@ exception NoSuchGoals of int
 (* This hook returns a string to be appended to the usual message.
    Primarily used to add a suggestion about the right bullet to use to
    focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> string option) ref = ref ((fun n -> None))
+let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ())
 let set_nosuchgoals_hook f = nosuchgoals_hook := f
 
 
@@ -358,10 +362,9 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f
 (* This uses the hook above *)
 let _ = Errors.register_handler begin function
   | NoSuchGoals n ->
-    let suffix:string option = (!nosuchgoals_hook) n in
+    let suffix = !nosuchgoals_hook n in
     Errors.errorlabstrm ""
-      (str "No such " ++ str (String.plural n "goal") ++ str "."
-       ++ pr_opt str suffix)
+      (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix)
   | _ -> raise Errors.Unhandled
 end
 
@@ -748,9 +751,15 @@ module Progress = struct
   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 (i1, c1, t1) (i2, c2, t2) =
-      Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 
-      && (eq_constr sigma1 sigma2) t1 t2
+    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 =
@@ -907,19 +916,11 @@ module Unsafe = struct
 
 end
 
+module UnsafeRepr = Proof.Unsafe
 
-
-(** {7 Notations} *)
-
-module Notations = struct
-  let (>>=) = tclBIND
-  let (<*>) = tclTHEN
-  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-end
-
-open Notations
-
-
+let (>>=) = tclBIND
+let (<*>) = tclTHEN
+let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
 
 (** {6 Goal-dependent tactics} *)
 
@@ -933,17 +934,20 @@ let catchable_exception = function
 
 module Goal = struct
 
-  type 'a t = {
+  type ('a, 'r) t = {
     env : Environ.env;
     sigma : Evd.evar_map;
     concl : Term.constr ;
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  let assume (gl : 'a t) = (gl :> [ `NF ] t)
+  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
+  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.V82.extra sigma self
@@ -969,7 +973,7 @@ module Goal = struct
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
+        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
@@ -987,7 +991,7 @@ module Goal = struct
     gmake_with info env sigma goal
 
   let enter f =
-    let f gl = InfoL.tag (Info.DBranch) (f gl) in
+    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 ->
@@ -999,6 +1003,41 @@ module Goal = struct
     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
@@ -1018,6 +1057,8 @@ module Goal = struct
   (* compatibility *)
   let goal { self=self } = self
 
+  let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t)
+
 end
 
 
@@ -1041,12 +1082,13 @@ struct
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
     (** Typecheck the hypotheses. *)
-    let type_hyp (sigma, env) (na, body, t as decl) =
+    let type_hyp (sigma, env) decl =
+      let t = get_type decl in
       let evdref = ref sigma in
-      let _ = Typing.sort_of env evdref t in
-      let () = match body with
-      | None -> ()
-      | Some body -> Typing.check env evdref body t
+      let _ = Typing.e_sort_of env evdref t in
+      let () = match decl with
+      | LocalAssum _ -> ()
+      | LocalDef (_,body,_) -> Typing.e_check env evdref body t
       in
       (!evdref, Environ.push_named decl env)
     in
@@ -1055,19 +1097,20 @@ struct
     let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
     (** Typecheck the conclusion *)
     let evdref = ref sigma in
-    let _ = Typing.sort_of env evdref (Evd.evar_concl info) in
+    let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
     !evdref
 
   let typecheck_proof c concl env sigma =
     let evdref = ref sigma in
-    let () = Typing.check env evdref c concl in
+    let () = Typing.e_check env evdref c concl in
     !evdref
 
   let (pr_constrv,pr_constr) =
     Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
-  let refine ?(unsafe = true) f = Goal.enter begin fun gl ->
+  let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl ->
     let sigma = Goal.sigma gl in
+    let sigma = Sigma.to_evar_map sigma in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
     (** Save the [future_goals] state to restore them after the
@@ -1075,7 +1118,7 @@ struct
     let prev_future_goals = Evd.future_goals sigma in
     let prev_principal_goal = Evd.principal_future_goal sigma in
     (** Create the refinement term *)
-    let (sigma, c) = f (Evd.reset_future_goals sigma) in
+    let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
     let evs = Evd.future_goals sigma in
     let evkmain = Evd.principal_future_goal sigma in
     (** Check that the introduced evars are well-typed *)
@@ -1106,7 +1149,7 @@ struct
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.modify (fun ps -> { ps with solution = sigma; comb; })
-  end
+  end }
 
   (** Useful definitions *)
 
@@ -1118,12 +1161,16 @@ struct
     in
     evd , j'.Environ.uj_val
 
-  let refine_casted ?unsafe f = Goal.enter begin fun gl ->
+  let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl ->
     let concl = Goal.concl gl in
     let env = Goal.env gl in
-    let f h = let (h, c) = f h in with_type env h c concl in
+    let f = { run = fun h ->
+      let Sigma (c, h, p) = f.run h in
+      let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
+      Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
+    } in
     refine ?unsafe f
-  end
+  end }
 end
 
 
@@ -1258,3 +1305,15 @@ module V82 = struct
       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