CLEANUP: Context.{Rel,Named}.Declaration.t

7 files changed, 70 insertions, 46 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1251dacd5..111a947a9 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -10,6 +10,7 @@ open Util
 open Pp
 open Term
 open Sigma.Notations
+open Context.Named.Declaration
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
@@ -76,7 +77,7 @@ module V82 = struct
     let evars = Sigma.to_evar_map evars in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
+    let inst = Array.map_of_list (mkVar % get_id) ctxt in
     let ev = Term.mkEvar (evk,inst) in
     (evk, ev, evars)
 
@@ -147,7 +148,7 @@ module V82 = struct
     let env = env sigma gl in
     let genv = Global.env () in
     let is_proof_var decl =
-      try ignore (Environ.lookup_named (Util.pi1 decl) genv); false
+      try ignore (Environ.lookup_named (get_id decl) genv); false
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 99e32db04..09f308abe 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -22,6 +22,7 @@ open Proof_type
 open Type_errors
 open Retyping
 open Misctypes
+open Context.Named.Declaration
 
 type refiner_error =
 
@@ -160,7 +161,8 @@ let reorder_context env sign ord =
       | _ ->
           (match ctxt_head with
             | [] -> error_no_such_hypothesis (List.hd ord)
-            | (x,_,_ as d) :: ctxt ->
+            | d :: ctxt ->
+                let x = get_id d in
                 if Id.Set.mem x expected then
                   step ord (Id.Set.remove x expected)
                     ctxt (push_item x d moved_hyps) ctxt_tail
@@ -175,7 +177,8 @@ let reorder_val_context env sign ord =
 
 
 
-let check_decl_position env sign (x,_,_ as d) =
+let check_decl_position env sign d =
+  let x = get_id d in
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
@@ -200,16 +203,17 @@ let move_location_eq m1 m2 = match m1, m2 with
 
 let rec get_hyp_after h = function
   | [] -> error_no_such_hypothesis h
-  | (hyp,_,_) :: right ->
-      if Id.equal hyp h then
-	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst
+  | d :: right ->
+      if Id.equal (get_id d) h then
+	match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst
       else
        get_hyp_after h right
 
 let split_sign hfrom hto l =
   let rec splitrec left toleft = function
     | [] -> error_no_such_hypothesis hfrom
-    | (hyp,c,typ) as d :: right ->
+    | d :: right ->
+        let hyp,_,typ = to_tuple d in
       	if Id.equal hyp hfrom then
 	  (left,right,d, toleft || move_location_eq hto MoveLast)
       	else
@@ -227,27 +231,28 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto =
+let move_hyp toleft (left,declfrom,right) hto =
   let env = Global.env() in
-  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
+  let test_dep d d2 =
     if toleft
-    then occur_var_in_decl env hyp2 d
-    else occur_var_in_decl env hyp d2
+    then occur_var_in_decl env (get_id d2) d
+    else occur_var_in_decl env (get_id d) d2
   in
   let rec moverec first middle = function
     | [] ->
 	if match hto with MoveFirst | MoveLast -> false | _ -> true then
 	  error_no_such_hypothesis (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
-    | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) ->
+    | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) ->
 	List.rev first @ List.rev middle @ right
-    | (hyp,_,_) as d :: right ->
+    | d :: right ->
+        let hyp = get_id d in
 	let (first',middle') =
       	  if List.exists (test_dep d) middle then
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
+	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
 	        Miscprint.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
@@ -483,12 +488,14 @@ and mk_casegoals sigma goal goalacc p c =
   (acc'',lbrty,conclty,sigma,p',c')
 
 
-let convert_hyp check sign sigma (id,b,bt as d) =
+let convert_hyp check sign sigma d =
+  let id,b,bt = to_tuple d in
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
     apply_to_hyp sign id
-      (fun _ (_,c,ct) _ ->
+      (fun _ d' _ ->
+        let _,c,ct = to_tuple d' in
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
 	  errorlabstrm "Logic.convert_hyp"
@@ -522,14 +529,14 @@ let prim_refiner r sigma goal =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
 	    let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
-	    move_hyp false ([],(id,None,t),named_context_of_val sign)
+	    move_hyp false ([], LocalAssum (id,t),named_context_of_val sign)
 	      nexthyp,
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
 	      errorlabstrm "Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
-	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
+	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
 	let oterm = Term.mkNamedLetIn id ev1 t ev2 in
@@ -546,7 +553,8 @@ let prim_refiner r sigma goal =
 		  with Not_found ->
 		    error "Cannot do a fixpoint on a non inductive type."
             	else
-		  check_ind (push_rel (na,None,c1) env) (k-1) b
+                  let open Context.Rel.Declaration in
+		  check_ind (push_rel (LocalAssum (na,c1)) env) (k-1) b
             | _ -> error "Not enough products."
 	in
 	let ((sp,_),u) = check_ind env n cl in
@@ -560,7 +568,7 @@ let prim_refiner r sigma goal =
 	      if !check && mem_named_context f (named_context_of_val sign) then
 		errorlabstrm "Logic.prim_refiner"
 		  (str "Name " ++ pr_id f ++ str " already used in the environment");
-	      mk_sign (push_named_context_val (f,None,ar) sign) oth
+	      mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth
 	  | [] ->
 	      Evd.Monad.List.map (fun (_,_,c) sigma ->
                 let gl,ev,sig' =
@@ -584,7 +592,8 @@ let prim_refiner r sigma goal =
      	let rec check_is_coind env cl =
 	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
-            | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
+            | Prod (na,c1,b) -> let open Context.Rel.Declaration in
+                                check_is_coind (push_rel (LocalAssum (na,c1)) env) b
             | _ ->
 		try
 		  let _ = find_coinductive env sigma b in ()
@@ -601,7 +610,7 @@ let prim_refiner r sigma goal =
                 error "Name already used in the environment.")
               with
               |	Not_found ->
-                  mk_sign (push_named_context_val (f,None,ar) sign) oth)
+                  mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth)
 	  | [] -> 
               Evd.Monad.List.map (fun (_,c) sigma ->
                 let gl,ev,sigma =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fc33e9a65..403a36141 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -267,18 +267,19 @@ let _ = Goptions.declare_bool_option
       Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
 
 let set_used_variables l =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
   let ctx_set =
-    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+    List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
   let aux env entry (ctx, all_safe, to_clear as orig) =
     match entry with
-    | (x,None,_) ->
+    | LocalAssum (x,_) ->
        if Id.Set.mem x all_safe then orig
        else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
-    | (x,Some bo, ty) as decl ->
+    | LocalDef (x,bo, ty) as decl ->
        if Id.Set.mem x all_safe then orig else
        let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
        if Id.Set.subset vars all_safe
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index a69645b11..681a7fa1a 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -10,6 +10,7 @@ open Names
 open Environ
 open Util
 open Vernacexpr
+open Context.Named.Declaration
 
 let to_string e =
   let rec aux = function
@@ -33,7 +34,8 @@ let in_nameset =
 
 let rec close_fwd e s =
   let s' =
-    List.fold_left (fun s (id,b,ty) ->      
+    List.fold_left (fun s decl ->
+      let (id,b,ty) = Context.Named.Declaration.to_tuple decl in
       let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
       let vty = global_vars_set e ty in
       let vbty = Id.Set.union vb vty in
@@ -61,13 +63,13 @@ and set_of_id env ty id =
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
   else if Id.to_string id = "All" then
-    List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+    List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
   else if CList.mem_assoc_f Id.equal id !known_names then
     process_expr env (CList.assoc_f Id.equal id !known_names) []
   else Id.Set.singleton id
 
 and full_set env =
-  List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+  List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
   let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 38e9cafad..5f4f414a4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -17,6 +17,7 @@ open Pp
 open Util
 open Proofview_monad
 open Sigma.Notations
+open Context.Named.Declaration
 
 (** Main state of tactics *)
 type proofview = Proofview_monad.proofview
@@ -750,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 =
@@ -1075,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.e_sort_of env evdref t in
-      let () = match body with
-      | None -> ()
-      | Some body -> Typing.e_check env evdref body t
+      let () = match decl with
+      | LocalAssum _ -> ()
+      | LocalDef (_,body,_) -> Typing.e_check env evdref body t
       in
       (!evdref, Environ.push_named decl env)
     in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8d6bdf6ae..186525e15 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -13,7 +13,7 @@ open Evd
 open Environ
 open Proof_type
 open Logic
-
+open Context.Named.Declaration
 
 let sig_it x = x.it
 let project x = x.sigma
@@ -202,7 +202,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   let { it = gls; sigma = sigma; } = rslt in
   let hyps:Context.Named.t list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
-  let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in
+  let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in
   let newhyps =
     List.map
       (fun hypl -> List.subtract cmp hypl oldhyps)
@@ -215,7 +215,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     List.fold_left
     (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
       ^ (List.fold_left
-	   (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc)
+	   (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
   pp (str (emacs_str "<infoH>")
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1e59c182c..33cef7486 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -19,6 +19,7 @@ open Proof_type
 open Logic
 open Refiner
 open Sigma.Notations
+open Context.Named.Declaration
 
 let re_sig it  gc = { it = it; sigma = gc; }
 
@@ -41,9 +42,11 @@ let pf_hyps  = Refiner.pf_hyps
 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
-  List.map (fun (id,_,x) -> (id, x)) sign
+  List.map (function LocalAssum (id,x)
+                   | LocalDef (id,_,x) -> id, x)
+           sign
 
-let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
+let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
@@ -54,8 +57,7 @@ let pf_get_hyp gls id =
     raise (RefinerError (NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
-  let (_,_,ty)= (pf_get_hyp gls id) in
-  ty
+  pf_get_hyp gls id |> get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
@@ -208,13 +210,14 @@ module New = struct
     sign
 
   let pf_get_hyp_typ id gl =
-    let (_,_,ty) = pf_get_hyp id gl in
-    ty
+    pf_get_hyp id gl |> get_type
 
   let pf_hyps_types gl =
     let env = Proofview.Goal.env gl in
     let sign = Environ.named_context env in
-    List.map (fun (id,_,x) -> (id, x)) sign
+    List.map (function LocalAssum (id,x)
+                     | LocalDef (id,_,x) -> id, x)
+             sign
 
   let pf_last_hyp gl =
     let hyps = Proofview.Goal.hyps gl in