details

src/core/env.ml

@@ -30,12 +30,12 @@ let find : string -> env -> tvar = fun n env ->
 (** [mem n env] returns [true] iff [n] is mapped to a variable in [env]. *)
 let mem : string -> env -> bool = List.mem_assoc
 
-(** [to_prod env t] builds a sequence of products / let-bindings whose domains
-    are the variables of the environment [env] (from left to right), and whose
-    body is the term [t]. By calling [to_prod [(xn,an,None);⋯;(x1,a1,None)] t]
-    you obtain a term of the form [Πx1:a1,..,Πxn:an,t]. *)
+(** [to_prod env t] builds a sequence of products whose domains are the
+    variables of the environment [env] (from left to right), and whose body is
+    the term [t]. By calling [to_prod [(xn,an,None);⋯;(x1,a1,None)] t] you
+    obtain a term of the form [Πx1:a1,..,Πxn:an,t]. *)
 let to_prod_box : env -> tbox -> tbox = fun env t ->
-  let add_prod t (_,(x,a,_u)) = _Prod a (Bindlib.bind_var x t) in
+  let add_prod t (_,(x,a,_)) = _Prod a (Bindlib.bind_var x t) in
   List.fold_left add_prod t env
 
 (** [to_prod] is an “unboxed” version of [to_prod_box]. *)

src/core/eval.ml

@@ -526,9 +526,9 @@ let whnf : reducer = fun ?tags c t ->
 
 let whnf = time_reducer whnf
 
-(** [simplify t] computes a beta whnf of [t] belonging to the set S such that:
-- terms of S are in beta whnf normal format
-- if [t] is a product, then both its domain and codomain are in S. *)
+(** [simplify c t] computes a beta whnf of [t] in context [c] belonging to the
+    set S such that (1) terms of S are in beta whnf normal format, (2) if [t]
+    is a product, then both its domain and codomain are in S. *)
 let simplify : ctxt -> term -> term = fun c ->
   let tags = [`NoRw; `NoExpand ] in
   let rec simp t =

src/core/eval.mli

@@ -65,9 +65,9 @@ val snf : ?dtree:(sym -> dtree) -> ?tags:rw_tag list -> ctxt -> term -> term
     context [c]. *)
 val hnf : ?tags:rw_tag list -> ctxt -> term -> term
 
-(** [simplify c t] computes a beta whnf of [t] belonging to the set S such
-    that (1) terms of S are in beta whnf normal format, (2) if [t] is a
-    product, then both its domain and codomain are in S. *)
+(** [simplify c t] computes a beta whnf of [t] in context [c] belonging to the
+    set S such that (1) terms of S are in beta whnf normal format, (2) if [t]
+    is a product, then both its domain and codomain are in S. *)
 val simplify : ctxt -> term -> term
 
 (** If [s] is a non-opaque symbol having a definition, [unfold_sym s t]

src/handle/tactic.ml

@@ -280,7 +280,7 @@ let rec handle :
       let p = new_problem() in
       let t = scope t in
       (* Generate the constraints for [t] to be of type [Type]. *)
-      let c = Env.to_ctxt gt.goal_hyps in
+      let c = Env.to_ctxt env in
       begin
         match Infer.check_noexn p c t mk_Type with
         | None -> fatal pos "%a is not of type Type." term t
@@ -305,21 +305,20 @@ let rec handle :
       check id;
       let p = new_problem() in
       let t = scope t in
-      let c = Env.to_ctxt gt.goal_hyps in
+      let c = Env.to_ctxt env in
       begin
         match Infer.infer_noexn p c t with
         | None -> fatal pos "%a is not typable." term t
         | Some (t,b) ->
           let x = new_tvar id.elt in
           let bt = lift t in
-          let e = gt.goal_hyps in
-          let e' = Env.add x (lift b) (Some bt) e in
+          let e' = Env.add x (lift b) (Some bt) env in
           let a = lift gt.goal_type in
           let m = LibMeta.fresh p (Env.to_prod e' a) (List.length e') in
-          let u = _Meta m (Array.append (Env.to_tbox e) [|bt|]) in
+          let u = _Meta m (Array.append (Env.to_tbox env) [|bt|]) in
           (*tac_refine pos ps gt gs p (Bindlib.unbox u)*)
           LibMeta.set p gt.goal_meta
-            (Bindlib.unbox (Bindlib.bind_mvar (Env.vars gt.goal_hyps) u));
+            (Bindlib.unbox (Bindlib.bind_mvar (Env.vars env) u));
           (*let g = Goal.of_meta m in*)
           let g = Typ {goal_meta=m; goal_hyps=e'; goal_type=gt.goal_type} in
           {ps with proof_goals = g :: gs}
@@ -349,11 +348,10 @@ let rec handle :
         | Unif _ -> assert false
         | Typ gt ->
             let k =
-              try List.pos (fun (s,_) -> s = id.elt) gt.goal_hyps
+              try List.pos (fun (s,_) -> s = id.elt) env
               with Not_found -> fatal id.pos "Unknown hypothesis."
             in
             let m = gt.goal_meta in
-            let env = gt.goal_hyps in
             let n = m.meta_arity - 1 in
             let a = cleanup !(m.meta_type) in (* cleanup necessary *)
             let b = LibTerm.codom_binder (n - k) a in
@@ -373,7 +371,7 @@ let rec handle :
       (* Reorder [ids] wrt their positions. *)
       let n = gt.goal_meta.meta_arity - 1 in
       let id_pos id =
-        try id, n - List.pos (fun (s,_) -> s = id.elt) gt.goal_hyps
+        try id, n - List.pos (fun (s,_) -> s = id.elt) env
         with Not_found -> fatal id.pos "Unknown hypothesis."
       in
       let cmp (_,k1) (_,k2) = Stdlib.compare k2 k1 in
@@ -397,7 +395,7 @@ let rec handle :
         let mt =
           mk_Appl(mk_Symb cfg.symb_P,
                   add_args (mk_Symb cfg.symb_eq) [a; r; l]) in
-        let meta_term = LibMeta.make p (Env.to_ctxt gt.goal_hyps) mt in
+        let meta_term = LibMeta.make p (Env.to_ctxt env) mt in
         (* The proofterm is [eqind a r l M (λx,eq a l x) (refl a l)]. *)
         Rewrite.swap cfg a r l meta_term
       in