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

11 files changed, 92 insertions, 86 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 041394d466..00ac2f56c3 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -111,7 +111,8 @@ type cofixpoint = constr pcofixpoint
 
 (** {6 Type of assumptions and contexts}  *)
 
-type rel_declaration = Name.t * constr option * constr
+type rel_declaration = LocalAssum of Name.t * constr          (* name, type *)
+                     | LocalDef of Name.t * constr * constr   (* name, value, type *)
 type rel_context = rel_declaration list
 
 (** The declarations below in .vo should be outside sections,
diff --git a/checker/closure.ml b/checker/closure.ml
index 400a535cf2..c2708e97d2 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -217,10 +217,10 @@ let ref_value_cache info ref =
 let defined_rels flags env =
 (*  if red_local_const (snd flags) then*)
   fold_rel_context
-      (fun (id,b,t) (i,subs) ->
-	 match b with
-	   | None -> (i+1, subs)
-	   | Some body -> (i+1, (i,body) :: subs))
+      (fun decl (i,subs) ->
+	 match decl with
+	   | LocalAssum _ -> (i+1, subs)
+	   | LocalDef (_,body,_) -> (i+1, (i,body) :: subs))
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 32d1713a88..3ce3125337 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -517,11 +517,8 @@ let map_decl_arity f g = function
   | RegularArity a -> RegularArity (f a)
   | TemplateArity a -> TemplateArity (g a)
 
-
-let subst_rel_declaration sub (id,copt,t as x) =
-  let copt' = Option.smartmap (subst_mps sub) copt in
-  let t' = subst_mps sub t in
-  if copt == copt' && t == t' then x else (id,copt',t')
+let subst_rel_declaration sub =
+  Term.map_rel_decl (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index f8f5c29b79..7040fdda46 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -80,7 +80,7 @@ let push_rel d env =
 let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 (* Universe constraints *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 2865f5bd4a..566df673c1 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -56,10 +56,10 @@ let is_constructor_head t =
 let conv_ctxt_prefix env (ctx1:rel_context) ctx2 =
   let rec chk env rctx1 rctx2 =
     match rctx1, rctx2 with
-        (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' ->
+        (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' ->
           conv env ty1 ty2;
           chk (push_rel d1 env) rctx1' rctx2'
-      | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' ->
+      | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' ->
           conv env ty1 ty2;
           conv env bd1 bd2;
           chk (push_rel d1 env) rctx1' rctx2'
@@ -94,10 +94,10 @@ let rec sorts_of_constr_args env t =
   match t with
     | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
 	varj :: sorts_of_constr_args env1 c2
     | LetIn (name,def,ty,c) ->
-        let env1 = push_rel (name,Some def,ty) env in
+        let env1 = push_rel (LocalDef (name,def,ty)) env in
 	sorts_of_constr_args env1 c
     | _ when is_constructor_head t -> []
     | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
@@ -167,7 +167,7 @@ let typecheck_arity env params inds =
 	   full_arity is used as argument or subject to cast, an
 	   upper universe will be generated *)
 	let id = ind.mind_typename in
-	let env_ar' = push_rel (Name id, None, arity) env_ar in
+	let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in
         env_ar')
       env
       inds in
@@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   let nhyps = List.length hyps in
   let rec check k index = function
     | [] -> ()
-    | (_,Some _,_)::hyps -> check k (index+1) hyps
+    | LocalDef _ :: hyps -> check k (index+1) hyps
     | _::hyps ->
         match whd_betadeltaiota env lpar.(k) with
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
@@ -340,7 +340,7 @@ let check_rec_par (env,n,_,_) hyps nrecp largs =
       | ([],_) -> ()
       | (_,[]) ->
           failwith "number of recursive parameters cannot be greater than the number of parameters."
-      | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps)
+      | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps)
       | (p::lp,_::hyps) ->
           (match whd_betadeltaiota env p with
 	    | Rel w when w = index -> find (index-1) (lp,hyps)
@@ -370,14 +370,15 @@ let abstract_mind_lc env ntyps npars lc =
    [lra] is the list of recursive tree of each variable
  *)
 let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
- (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+ (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
   let auxntyp = 1 in
   let specif = lookup_mind_specif env mi in
   let env' =
-    push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in
+    let decl = LocalAssum (Anonymous,
+                           hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in
+    push_rel decl env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 79dba4fac5..5e2e14f7fb 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -88,10 +88,10 @@ let instantiate_params full t u args sign =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
     fold_rel_context
-      (fun (_,copt,_) (largs,subs,ty) ->
-        match (copt, largs, ty) with
-          | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
-          | (Some b,_,LetIn(_,_,_,t))    -> 
+      (fun decl (largs,subs,ty) ->
+        match (decl, largs, ty) with
+          | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+          | (LocalDef (_,b,_),_,LetIn(_,_,_,t))    ->
 	    (largs, (substl subs (subst_instance_constr u b))::subs, t)
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
@@ -161,7 +161,7 @@ let remember_subst u subst =
 (* Propagate the new levels in the signature *)
 let rec make_subst env =
   let rec make subst = function
-    | (_,Some _,_)::sign, exp, args ->
+    | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
     | d::sign, None::exp, args ->
         let args = match args with _::args -> args | [] -> [] in
@@ -174,7 +174,7 @@ let rec make_subst env =
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env a)) in
         make (cons_subst u s subst) (sign, exp, args)
-    | (na,None,t)::sign, Some u::exp, [] ->
+    | LocalAssum (na,t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
         (* template, it is identity substitution  otherwise (ie. when u is *)
@@ -319,8 +319,8 @@ let elim_sorts (_,mip) = mip.mind_kelim
 
 let extended_rel_list n hyps =
   let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | LocalDef _ :: hyps -> reln l (p+1) hyps
     | [] -> l
   in
   reln [] 1 hyps
@@ -345,12 +345,12 @@ let is_correct_arity env c (p,pj) ind specif params =
   let rec srec env pt ar =
     let pt' = whd_betadeltaiota env pt in
     match pt', ar with
-      | Prod (na1,a1,t), (_,None,a1')::ar' ->
+      | Prod (na1,a1,t), LocalAssum (_,a1')::ar' ->
           (try conv env a1 a1'
           with NotConvertible -> raise (LocalArity None));
-          srec (push_rel (na1,None,a1) env) t ar'
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
-	 let env' = push_rel (na1,None,a1) env in
+	 let env' = push_rel (LocalAssum (na1,a1)) env in
      let ksort = match (whd_betadeltaiota env' a2) with
         | Sort s -> family_of_sort s
 	    | _ -> raise (LocalArity None) in
@@ -362,8 +362,8 @@ let is_correct_arity env c (p,pj) ind specif params =
       | Sort s', [] ->
 	  check_allowed_sort (family_of_sort s') specif;
 	  false
-      | _, (_,Some _,_ as d)::ar' ->
-	 srec (push_rel d env) (lift 1 pt') ar'
+      | _, (LocalDef _ as d)::ar' ->
+         srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
 	  raise (LocalArity None)
   in
@@ -530,7 +530,7 @@ let make_renv env recarg tree =
     genv = [Lazy.lazy_from_val(Subterm(Large,tree))] }
 
 let push_var renv (x,ty,spec) =
-  { env = push_rel (x,None,ty) renv.env;
+  { env = push_rel (LocalAssum (x,ty)) renv.env;
     rel_min = renv.rel_min+1;
     genv = spec:: renv.genv }
 
@@ -628,14 +628,15 @@ let check_inductive_codomain env p =
 (* The following functions are almost duplicated from indtypes.ml, except
 that they carry here a poorer environment (containing less information). *)
 let ienv_push_var (env, lra) (x,a,ra) =
-(push_rel (x,None,a) env, (Norec,ra)::lra)
+(push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind specif env =
-     push_rel (Anonymous,None,
-		hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env
+     let decl = LocalAssum (Anonymous,
+		            hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+     push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
   let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
@@ -902,7 +903,7 @@ let filter_stack_domain env ci p stack =
     let t = whd_betadeltaiota env ar in
     match stack, t with
     | elt :: stack', Prod (n,a,c0) ->
-      let d = (n,None,a) in
+      let d = LocalAssum (n,a) in
       let ty, args = decompose_app (whd_betadeltaiota env a) in
       let elt = match ty with
       | Ind ind -> 
@@ -956,10 +957,10 @@ let check_one_fix renv recpos trees def =
               end
             else
               begin
-                match pi2 (lookup_rel p renv.env) with
-                | None ->
+                match lookup_rel p renv.env with
+                | LocalAssum _ ->
                     List.iter (check_rec_call renv []) l
-                | Some c ->
+                | LocalDef (_,c,_) ->
                     try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
                       check_rec_call renv stack (applist(lift p c,l))
@@ -1078,7 +1079,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
       match (whd_betadeltaiota env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
-	      let env' = push_rel (x, None, a) env in
+	      let env' = push_rel (LocalAssum (x,a)) env in
               if n = k+1 then
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) =
@@ -1127,7 +1128,7 @@ let rec codomain_is_coind env c =
   let b = whd_betadeltaiota env c in
   match b with
     | Prod (x,a,b) ->
-	codomain_is_coind (push_rel (x, None, a) env) b
+	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
 	(try find_coinductive env b
         with Not_found ->
@@ -1168,7 +1169,7 @@ let check_one_cofix env nbfix def deftype =
 	| Lambda (x,a,b) ->
 	     assert (args = []);
             if noccur_with_meta n nbfix a then
-              let env' = push_rel (x, None, a) env in
+              let env' = push_rel (LocalAssum (x,a)) env in
               check_rec_call env' alreadygrd (n+1) tree vlra b
             else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 3a666a60a4..f1aa5d9194 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -490,7 +490,7 @@ let dest_prod env =
     let t = whd_betadeltaiota env c in
     match t with
       | Prod (n,a,c0) ->
-          let d = (n,None,a) in
+          let d = LocalAssum (n,a) in
 	  decrec (push_rel d env) (d::m) c0
       | _ -> m,t
   in
@@ -502,10 +502,10 @@ let dest_prod_assum env =
     let rty = whd_betadeltaiota_nolet env ty in
     match rty with
     | Prod (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	prodec_rec (push_rel d env) (d::l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	prodec_rec (push_rel d env) (d::l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
@@ -520,10 +520,10 @@ let dest_lam_assum env =
     let rty = whd_betadeltaiota_nolet env ty in
     match rty with
     | Lambda (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	lamec_rec (push_rel d env) (d::l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	lamec_rec (push_rel d env) (d::l) c
     | Cast (c,_,_)    -> lamec_rec env l c
     | _               -> l,rty
diff --git a/checker/term.ml b/checker/term.ml
index 6487d1a152..56cc9cdc22 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -222,24 +222,29 @@ let rel_context_length = List.length
 let rel_context_nhyps hyps =
   let rec nhyps acc = function
     | [] -> acc
-    | (_,None,_)::hyps -> nhyps (1+acc) hyps
-    | (_,Some _,_)::hyps -> nhyps acc hyps in
+    | LocalAssum _ :: hyps -> nhyps (1+acc) hyps
+    | LocalDef _ :: hyps -> nhyps acc hyps in
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
-let map_rel_context f l =
-  let map_decl (n, body_o, typ as decl) =
-    let body_o' = Option.smartmap f body_o in
-    let typ' = f typ in
-      if body_o' == body_o && typ' == typ then decl else
-	(n, body_o', typ')
-  in
-    List.smartmap map_decl l
+let map_rel_decl f = function
+  | LocalAssum (n, typ) as decl ->
+     let typ' = f typ in
+     if typ' == typ then decl else
+       LocalAssum (n, typ')
+  | LocalDef (n, body, typ) as decl ->
+     let body' = f body in
+     let typ' = f typ in
+     if body' == body && typ' == typ then decl else
+       LocalDef (n, body', typ')
+
+let map_rel_context f =
+  List.smartmap (map_rel_decl f)
 
 let extended_rel_list n hyps =
   let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | LocalDef _ :: hyps -> reln l (p+1) hyps
     | [] -> l
   in
   reln [] 1 hyps
@@ -272,8 +277,8 @@ let decompose_lam_n_assum n =
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
-    | Lambda (x,t,c)  -> lamdec_rec ((x,None,t) :: l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
+    | Lambda (x,t,c)  -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c
     | Cast (c,_,_)      -> lamdec_rec l n c
     | c -> error "decompose_lam_n_assum: not enough abstractions"
   in
@@ -282,18 +287,18 @@ let decompose_lam_n_assum n =
 (* Iterate products, with or without lets *)
 
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
-let mkProd_or_LetIn (na,body,t) c =
-  match body with
-    | None -> Prod (na, t, c)
-    | Some b -> LetIn (na, b, t, c)
+let mkProd_or_LetIn decl c =
+  match decl with
+    | LocalAssum (na,t) -> Prod (na, t, c)
+    | LocalDef (na,b,t) -> LetIn (na, b, t, c)
 
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 
 let decompose_prod_assum =
   let rec prodec_rec l c =
     match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | _               -> l,c
   in
@@ -305,8 +310,8 @@ let decompose_prod_n_assum n =
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) (n-1) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c
     | Cast (c,_,_)    -> prodec_rec l n c
     | c -> error "decompose_prod_n_assum: not enough assumptions"
   in
@@ -324,8 +329,8 @@ let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
 let destArity =
   let rec prodec_rec l c =
     match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t)::l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | Sort s          -> l,s
     | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
diff --git a/checker/term.mli b/checker/term.mli
index ab488b2b7c..0af83e05d7 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -35,12 +35,13 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
 val compose_lam : (name * constr) list -> constr -> constr
 val decompose_lam : constr -> (name * constr) list * constr
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
-val mkProd_or_LetIn : name * constr option * constr -> constr -> constr
+val mkProd_or_LetIn : rel_declaration -> constr -> constr
 val it_mkProd_or_LetIn : constr -> rel_context -> constr
 val decompose_prod_assum : constr -> rel_context * constr
 val decompose_prod_n_assum : int -> constr -> rel_context * constr
diff --git a/checker/typeops.ml b/checker/typeops.ml
index d49c40a8bd..64afd21b2a 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -62,7 +62,7 @@ let judge_of_type u = Sort (Type (Univ.super u))
 
 let judge_of_relative env n =
   try
-    let (_,_,typ) = lookup_rel n env in
+    let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in
     lift n typ
   with Not_found ->
     error_unbound_rel env n
@@ -296,13 +296,13 @@ let rec execute env cstr =
 
     | Lambda (name,c1,c2) ->
         let _ = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let j' = execute env1 c2 in
         Prod(name,c1,j')
 
     | Prod (name,c1,c2) ->
         let varj = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let varj' = execute_type env1 c2 in
 	Sort (sort_of_product env varj varj')
 
@@ -314,7 +314,7 @@ let rec execute env cstr =
           let env',c2' = (* refresh_arity env *) env, c2 in
           let _ = execute_type env' c2' in
           judge_of_cast env' (c1,j1) DEFAULTcast c2' in
-        let env1 = push_rel (name,Some c1,c2) env in
+        let env1 = push_rel (LocalDef (name,c1,c2)) env in
         let j' = execute env1 c3 in
         subst1 c1 j'
 
@@ -378,10 +378,10 @@ let infer_type env constr = execute_type env constr
 let check_ctxt env rels =
   fold_rel_context (fun d env ->
     match d with
-        (_,None,ty) ->
+      | LocalAssum (_,ty) ->
           let _ = infer_type env ty in
           push_rel d env
-      | (_,Some bd,ty) ->
+      | LocalDef (_,bd,ty) ->
           let j1 = infer env bd in
           let _ = infer env ty in
           conv_leq env j1 ty;
@@ -399,9 +399,9 @@ let check_polymorphic_arity env params par =
   let pl = par.template_param_levels in
   let rec check_p env pl params =
     match pl, params with
-        Some u::pl, (na,None,ty)::params ->
+        Some u::pl, LocalAssum (na,ty)::params ->
           check_kind env ty u;
-          check_p (push_rel (na,None,ty) env) pl params
+          check_p (push_rel (LocalAssum (na,ty)) env) pl params
       | None::pl,d::params -> check_p (push_rel d env) pl params
       | [], _ -> ()
       | _ -> failwith "check_poly: not the right number of params" in
diff --git a/checker/values.ml b/checker/values.ml
index c14e9223da..19cbb50606 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 7c050ff1db22f14ee3a4c44aae533082 checker/cic.mli
+MD5 9f7fd499f812b6548a55f7067e6a9d06 checker/cic.mli
 
 *)
 
@@ -154,8 +154,8 @@ and v_prec = Tuple ("prec_declaration",
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
 
-
-let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|]
+let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|];               (* LocalAssum *)
+                                           [|v_name; v_constr; v_constr|] |]   (* LocalDef *)
 let v_rctxt = List v_rdecl
 
 let v_section_ctxt = v_enum "emptylist" 1