Imported Upstream version 8.5~beta1+dfsg

1 files changed, 227 insertions, 187 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 8b27cf91..2642b186 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -1,36 +1,40 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
 open Term
+open Vars
+open Context
 open Declarations
-open Sign
 open Environ
 open Entries
 open Reduction
 open Inductive
 open Type_errors
 
-let conv_leq l2r = default_conv CUMUL ~l2r
+let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
 
 let conv_leq_vecti env v1 v2 =
-  array_fold_left2_i
-    (fun i c t1 t2 ->
-      let c' =
-        try default_conv CUMUL env t1 t2
-        with NotConvertible -> raise (NotConvertibleVect i) in
-      union_constraints c c')
-    empty_constraint
+  Array.fold_left2_i
+    (fun i _ t1 t2 ->
+      try conv_leq false env t1 t2
+      with NotConvertible -> raise (NotConvertibleVect i))
+    ()
     v1
     v2
 
+let check_constraints cst env = 
+  if Environ.check_constraints cst env then ()
+  else error_unsatisfied_constraints env cst
+
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env j =
   match kind_of_term(whd_betadeltaiota env j.uj_type) with
@@ -67,9 +71,9 @@ let judge_of_prop_contents = function
 (* Type of Type(i). *)
 
 let judge_of_type u =
-  let uu = super u in
-  { uj_val = mkType u;
-    uj_type = mkType uu }
+  let uu = Universe.super u in
+    { uj_val = mkType u;
+      uj_type = mkType uu }
 
 (*s Type of a de Bruijn index. *)
 
@@ -91,82 +95,106 @@ let judge_of_variable env id =
 
 (* Management of context of variables. *)
 
-(* Checks if a context of variable can be instantiated by the
-   variables of the current env *)
-(* TODO: check order? *)
-let rec check_hyps_inclusion env sign =
-  Sign.fold_named_context
-    (fun (id,_,ty1) () ->
-      let ty2 = named_type id env in
-      if not (eq_constr ty2 ty1) then
-        error "types do not match")
+(* Checks if a context of variables can be instantiated by the
+   variables of the current env.
+   Order does not have to be checked assuming that all names are distinct *)
+let check_hyps_inclusion env c sign =
+  Context.fold_named_context
+    (fun (id,b1,ty1) () ->
+      try
+        let (_,b2,ty2) = lookup_named id env in
+        conv env ty2 ty1;
+        (match b2,b1 with
+        | None, None -> ()
+        | None, Some _ ->
+            (* This is wrong, because we don't know if the body is
+               needed or not for typechecking: *) ()
+        | Some _, None -> raise NotConvertible
+        | Some b2, Some b1 -> conv env b2 b1);
+      with Not_found | NotConvertible | Option.Heterogeneous ->
+        error_reference_variables env id c)
     sign
     ~init:()
 
-
-let check_args env c hyps =
-  try check_hyps_inclusion env hyps
-  with UserError _ | Not_found ->
-    error_reference_variables env c
-
-
-(* Checks if the given context of variables [hyps] is included in the
-   current context of [env]. *)
-(*
-let check_hyps id env hyps =
-  let hyps' = named_context env in
-  if not (hyps_inclusion env hyps hyps') then
-    error_reference_variables env id
-*)
 (* Instantiation of terms on real arguments. *)
 
 (* Make a type polymorphic if an arity *)
 
 let extract_level env p =
   let _,c = dest_prod_assum env p in
-  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+  match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
 
-let extract_context_levels env =
-  List.fold_left
-    (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
+let extract_context_levels env l =
+  let fold l (_, b, p) = match b with
+  | None -> extract_level env p :: l
+  | _ -> l
+  in
+  List.fold_left fold [] l
 
 let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
   match kind_of_term ccl with
   | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
       let param_ccls = extract_context_levels env params in
-      let s = { poly_param_levels = param_ccls; poly_level = u} in
-      PolymorphicArity (params,s)
+      let s = { template_param_levels = param_ccls; template_level = u} in
+      TemplateArity (params,s)
   | _ ->
-      NonPolymorphicType t
+      RegularArity t
 
 (* Type of constants *)
 
-let type_of_constant_knowing_parameters env t paramtyps =
+let type_of_constant_type_knowing_parameters env t paramtyps =
   match t with
-  | NonPolymorphicType t -> t
-  | PolymorphicArity (sign,ar) ->
+  | RegularArity t -> t
+  | TemplateArity (sign,ar) ->
       let ctx = List.rev sign in
       let ctx,s = instantiate_universes env ctx ar paramtyps in
       mkArity (List.rev ctx,s)
 
+let type_of_constant_knowing_parameters env cst paramtyps =
+  let cb = lookup_constant (fst cst) env in
+  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let ty, cu = constant_type env cst in
+    type_of_constant_type_knowing_parameters env ty paramtyps, cu
+
+let type_of_constant_knowing_parameters_in env cst paramtyps =
+  let cb = lookup_constant (fst cst) env in
+  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let ty = constant_type_in env cst in
+    type_of_constant_type_knowing_parameters env ty paramtyps
+
 let type_of_constant_type env t =
-  type_of_constant_knowing_parameters env t [||]
+  type_of_constant_type_knowing_parameters env t [||]
 
 let type_of_constant env cst =
-  type_of_constant_type env (constant_type env cst)
+  type_of_constant_knowing_parameters env cst [||]
 
-let judge_of_constant_knowing_parameters env cst jl =
-  let c = mkConst cst in
-  let cb = lookup_constant cst env in
-  let _ = check_args env c cb.const_hyps in
-  let paramstyp = Array.map (fun j -> j.uj_type) jl in
-  let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in
-  make_judge c t
+let type_of_constant_in env cst =
+  let cb = lookup_constant (fst cst) env in
+  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let ar = constant_type_in env cst in
+    type_of_constant_type_knowing_parameters env ar [||]
+
+let judge_of_constant_knowing_parameters env (kn,u as cst) args =
+  let c = mkConstU cst in
+  let ty, cu = type_of_constant_knowing_parameters env cst args in
+  let _ = Environ.check_constraints cu env in
+    make_judge c ty
 
 let judge_of_constant env cst =
   judge_of_constant_knowing_parameters env cst [||]
 
+let type_of_projection env (p,u) =
+  let cst = Projection.constant p in
+  let cb = lookup_constant cst env in
+  match cb.const_proj with
+  | Some pb -> 
+    if cb.const_polymorphic then
+      Vars.subst_instance_constr u pb.proj_type
+    else pb.proj_type
+  | None -> raise (Invalid_argument "type_of_projection: not a projection")
+
+
 (* Type of a lambda-abstraction. *)
 
 (* [judge_of_abstraction env name var j] implements the rule
@@ -192,18 +220,16 @@ let judge_of_letin env name defj typj j =
 (* Type of an application. *)
 
 let judge_of_apply env funj argjv =
-  let rec apply_rec n typ cst = function
+  let rec apply_rec n typ = function
     | [] ->
 	{ uj_val  = mkApp (j_val funj, Array.map j_val argjv);
-          uj_type = typ },
-	cst
+          uj_type = typ }
     | hj::restjl ->
         (match kind_of_term (whd_betadeltaiota env typ) with
           | Prod (_,c1,c2) ->
 	      (try
-		let c = conv_leq false env hj.uj_type c1 in
-		let cst' = union_constraints cst c in
-		apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
+		 let () = conv_leq false env hj.uj_type c1 in
+		   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
 	      with NotConvertible ->
 		error_cant_apply_bad_type env
 		  (n,c1, hj.uj_type)
@@ -214,7 +240,6 @@ let judge_of_apply env funj argjv =
   in
   apply_rec 1
     funj.uj_type
-    empty_constraint
     (Array.to_list argjv)
 
 (* Type of product *)
@@ -227,18 +252,20 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if engagement env = Some ImpredicativeSet then
+        begin match engagement env with
+        | Some ImpredicativeSet ->
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        else
+        | _ ->
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (sup u1 type0_univ)
+          Type (Universe.sup Universe.type0 u1)
+        end
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
+    | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (sup u1 u2)
+    | (Type u1, Type u2) -> Type (Universe.sup u1 u2)
 
 (* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule
 
@@ -272,13 +299,17 @@ let judge_of_cast env cj k tj =
           vm_conv CUMUL env cj.uj_type expected_type
       | DEFAULTcast ->
           mkCast (cj.uj_val, k, expected_type),
-          conv_leq false env cj.uj_type expected_type
+          default_conv ~l2r:false CUMUL env cj.uj_type expected_type
       | REVERTcast ->
           cj.uj_val,
-          conv_leq true env cj.uj_type expected_type in
-    { uj_val = c;
-      uj_type = expected_type },
-    cst
+          default_conv ~l2r:true CUMUL env cj.uj_type expected_type
+      | NATIVEcast ->
+	 let sigma = Nativelambda.empty_evars in
+         mkCast (cj.uj_val, k, expected_type),
+         native_conv CUMUL sigma env cj.uj_type expected_type
+    in
+      { uj_val = c;
+	uj_type = expected_type }
   with NotConvertible ->
     error_actual_type env cj expected_type
 
@@ -296,50 +327,70 @@ let judge_of_cast env cj k tj =
    the App case of execute; from this constraints, the expected
    dynamic constraints of the form u<=v are enforced *)
 
-let judge_of_inductive_knowing_parameters env ind jl =
-  let c = mkInd ind in
-  let (mib,mip) = lookup_mind_specif env ind in
-  check_args env c mib.mind_hyps;
-  let paramstyp = Array.map (fun j -> j.uj_type) jl in
-  let t = Inductive.type_of_inductive_knowing_parameters env mip paramstyp in
-  make_judge c t
+let judge_of_inductive_knowing_parameters env (ind,u as indu) args =
+  let c = mkIndU indu in
+  let (mib,mip) as spec = lookup_mind_specif env ind in
+  check_hyps_inclusion env c mib.mind_hyps;
+  let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters 
+    env (spec,u) args
+  in
+    check_constraints cst env;
+    make_judge c t
 
-let judge_of_inductive env ind =
-  judge_of_inductive_knowing_parameters env ind [||]
+let judge_of_inductive env (ind,u as indu) =
+  let c = mkIndU indu in
+  let (mib,mip) as spec = lookup_mind_specif env ind in
+  check_hyps_inclusion env c mib.mind_hyps;
+  let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in
+    check_constraints cst env;
+    (make_judge c t)
 
 (* Constructors. *)
 
-let judge_of_constructor env c =
-  let constr = mkConstruct c in
+let judge_of_constructor env (c,u as cu) =
+  let constr = mkConstructU cu in
   let _ =
     let ((kn,_),_) = c in
     let mib = lookup_mind kn env in
-    check_args env constr mib.mind_hyps in
+    check_hyps_inclusion env constr mib.mind_hyps in
   let specif = lookup_mind_specif env (inductive_of_constructor c) in
-  make_judge constr (type_of_constructor c specif)
+  let t,cst = constrained_type_of_constructor cu specif in
+  let () = check_constraints cst env in
+    (make_judge constr t)
 
 (* Case. *)
 
-let check_branch_types env ind cj (lfj,explft) =
+let check_branch_types env (ind,u) cj (lfj,explft) =
   try conv_leq_vecti env (Array.map j_type lfj) explft
   with
       NotConvertibleVect i ->
-        error_ill_formed_branch env cj.uj_val (ind,i+1) lfj.(i).uj_type explft.(i)
+        error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
     | Invalid_argument _ ->
         error_number_branches env cj (Array.length explft)
 
 let judge_of_case env ci pj cj lfj =
-  let indspec =
+  let (pind, _ as indspec) =
     try find_rectype env cj.uj_type
     with Not_found -> error_case_not_inductive env cj in
-  let _ = check_case_info env (fst indspec) ci in
-  let (bty,rslty,univ) =
+  let _ = check_case_info env pind ci in
+  let (bty,rslty) =
     type_case_branches env indspec pj cj.uj_val in
-  let univ' = check_branch_types env (fst indspec) cj (lfj,bty) in
+  let () = check_branch_types env pind cj (lfj,bty) in
   ({ uj_val  = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val,
                        Array.map j_val lfj);
-     uj_type = rslty },
-  union_constraints univ univ')
+     uj_type = rslty })
+
+let judge_of_projection env p cj =
+  let pb = lookup_projection p env in
+  let (ind,u), args =
+    try find_rectype env cj.uj_type
+    with Not_found -> error_case_not_inductive env cj
+  in
+    assert(eq_mind pb.proj_ind (fst ind));
+    let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
+    let ty = substl (cj.uj_val :: List.rev args) ty in
+      {uj_val = mkProj (p,cj.uj_val);
+       uj_type = ty}
 
 (* Fixpoints. *)
 
@@ -348,7 +399,7 @@ let judge_of_case env ci pj cj lfj =
 
 let type_fixpoint env lna lar vdefj =
   let lt = Array.length vdefj in
-  assert (Array.length lar = lt);
+  assert (Int.equal (Array.length lar) lt);
   try
     conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar)
   with NotConvertibleVect i ->
@@ -357,166 +408,155 @@ let type_fixpoint env lna lar vdefj =
 (************************************************************************)
 (************************************************************************)
 
-(* This combinator adds the universe constraints both in the local
-   graph and in the universes of the environment. This is to ensure
-   that the infered local graph is satisfiable. *)
-let univ_combinator (cst,univ) (j,c') =
-  (j,(union_constraints cst c', merge_constraints c' univ))
-
 (* The typing machine. *)
     (* ATTENTION : faudra faire le typage du contexte des Const,
     Ind et Constructsi un jour cela devient des constructions
     arbitraires et non plus des variables *)
-let rec execute env cstr cu =
+let rec execute env cstr =
   match kind_of_term cstr with
     (* Atomic terms *)
     | Sort (Prop c) ->
-	(judge_of_prop_contents c, cu)
-
+      judge_of_prop_contents c
+	
     | Sort (Type u) ->
-	(judge_of_type u, cu)
+      judge_of_type u
 
     | Rel n ->
-	(judge_of_relative env n, cu)
+      judge_of_relative env n
 
     | Var id ->
-	(judge_of_variable env id, cu)
+      judge_of_variable env id
 
     | Const c ->
-        (judge_of_constant env c, cu)
+      judge_of_constant env c
+	
+    | Proj (p, c) ->
+        let cj = execute env c in
+          judge_of_projection env p cj
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let (jl,cu1) = execute_array env args cu in
-	let (j,cu2) =
+        let jl = execute_array env args in
+	let j =
 	  match kind_of_term f with
-	    | Ind ind ->
+	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
-		judge_of_inductive_knowing_parameters env ind jl, cu1
-	    | Const cst ->
+	      let args = Array.map (fun j -> lazy j.uj_type) jl in
+		judge_of_inductive_knowing_parameters env ind args
+	    | Const cst when Environ.template_polymorphic_pconstant cst env ->
 		(* Sort-polymorphism of constant *)
-		judge_of_constant_knowing_parameters env cst jl, cu1
+	      let args = Array.map (fun j -> lazy j.uj_type) jl in
+		judge_of_constant_knowing_parameters env cst args
 	    | _ ->
 		(* No sort-polymorphism *)
-		execute env f cu1
+		execute env f
 	in
-	univ_combinator cu2 (judge_of_apply env j jl)
+	  judge_of_apply env j jl
 
     | Lambda (name,c1,c2) ->
-        let (varj,cu1) = execute_type env c1 cu in
-	let env1 = push_rel (name,None,varj.utj_val) env in
-        let (j',cu2) = execute env1 c2 cu1 in
-        (judge_of_abstraction env name varj j', cu2)
+      let varj = execute_type env c1 in
+      let env1 = push_rel (name,None,varj.utj_val) env in
+      let j' = execute env1 c2 in
+        judge_of_abstraction env name varj j'
 
     | Prod (name,c1,c2) ->
-        let (varj,cu1) = execute_type env c1 cu in
-	let env1 = push_rel (name,None,varj.utj_val) env in
-        let (varj',cu2) = execute_type env1 c2 cu1 in
-	(judge_of_product env name varj varj', cu2)
+      let varj = execute_type env c1 in
+      let env1 = push_rel (name,None,varj.utj_val) env in
+      let varj' = execute_type env1 c2 in
+	judge_of_product env name varj varj'
 
     | LetIn (name,c1,c2,c3) ->
-        let (j1,cu1) = execute env c1 cu in
-        let (j2,cu2) = execute_type env c2 cu1 in
-        let (_,cu3) =
-	  univ_combinator cu2 (judge_of_cast env j1 DEFAULTcast j2) in
-        let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
-        let (j',cu4) = execute env1 c3 cu3 in
-        (judge_of_letin env name j1 j2 j', cu4)
+      let j1 = execute env c1 in
+      let j2 = execute_type env c2 in
+      let _ = judge_of_cast env j1 DEFAULTcast j2 in
+      let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
+      let j' = execute env1 c3 in
+        judge_of_letin env name j1 j2 j'
 
     | Cast (c,k, t) ->
-        let (cj,cu1) = execute env c cu in
-        let (tj,cu2) = execute_type env t cu1 in
-	univ_combinator cu2
-          (judge_of_cast env cj k tj)
+      let cj = execute env c in
+      let tj = execute_type env t in
+        judge_of_cast env cj k tj
 
     (* Inductive types *)
     | Ind ind ->
-	(judge_of_inductive env ind, cu)
+      judge_of_inductive env ind
 
     | Construct c ->
-	(judge_of_constructor env c, cu)
+      judge_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let (cj,cu1) = execute env c cu in
-        let (pj,cu2) = execute env p cu1 in
-        let (lfj,cu3) = execute_array env lf cu2 in
-        univ_combinator cu3
-          (judge_of_case env ci pj cj lfj)
+        let cj = execute env c in
+        let pj = execute env p in
+        let lfj = execute_array env lf in
+          judge_of_case env ci pj cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
-        let ((fix_ty,recdef'),cu1) = execute_recdef env recdef i cu in
-        let fix = (vni,recdef') in
+      let (fix_ty,recdef') = execute_recdef env recdef i in
+      let fix = (vni,recdef') in
         check_fix env fix;
-	(make_judge (mkFix fix) fix_ty, cu1)
-
+	make_judge (mkFix fix) fix_ty
+	  
     | CoFix (i,recdef) ->
-        let ((fix_ty,recdef'),cu1) = execute_recdef env recdef i cu in
-        let cofix = (i,recdef') in
+      let (fix_ty,recdef') = execute_recdef env recdef i in
+      let cofix = (i,recdef') in
         check_cofix env cofix;
-	(make_judge (mkCoFix cofix) fix_ty, cu1)
-
+	(make_judge (mkCoFix cofix) fix_ty)
+	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
-	anomaly "the kernel does not support metavariables"
+	anomaly (Pp.str "the kernel does not support metavariables")
 
     | Evar _ ->
-	anomaly "the kernel does not support existential variables"
+	anomaly (Pp.str "the kernel does not support existential variables")
 
-and execute_type env constr cu =
-  let (j,cu1) = execute env constr cu in
-  (type_judgment env j, cu1)
+and execute_type env constr =
+  let j = execute env constr in
+    type_judgment env j
 
-and execute_recdef env (names,lar,vdef) i cu =
-  let (larj,cu1) = execute_array env lar cu in
+and execute_recdef env (names,lar,vdef) i =
+  let larj = execute_array env lar in
   let lara = Array.map (assumption_of_judgment env) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let (vdefj,cu2) = execute_array env1 vdef cu1 in
+  let vdefj = execute_array env1 vdef in
   let vdefv = Array.map j_val vdefj in
-  let cst = type_fixpoint env1 names lara vdefj in
-  univ_combinator cu2
-    ((lara.(i),(names,lara,vdefv)),cst)
+  let () = type_fixpoint env1 names lara vdefj in
+    (lara.(i),(names,lara,vdefv))
 
-and execute_array env = array_fold_map' (execute env)
+and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
 let infer env constr =
-  let (j,(cst,_)) =
-    execute env constr (empty_constraint, universes env) in
-  assert (eq_constr j.uj_val constr);
-  (j, cst)
+  let j = execute env constr in
+    assert (eq_constr j.uj_val constr);
+    j
+
+(* let infer_key = Profile.declare_profile "infer" *)
+(* let infer = Profile.profile2 infer_key infer *)
 
 let infer_type env constr =
-  let (j,(cst,_)) =
-    execute_type env constr (empty_constraint, universes env) in
-  (j, cst)
+  let j = execute_type env constr in
+    j
 
 let infer_v env cv =
-  let (jv,(cst,_)) =
-    execute_array env cv (empty_constraint, universes env) in
-  (jv, cst)
+  let jv = execute_array env cv in
+    jv
 
 (* Typing of several terms. *)
 
 let infer_local_decl env id = function
   | LocalDef c ->
-      let (j,cst) = infer env c in
-      (Name id, Some j.uj_val, j.uj_type), cst
+      let j = infer env c in
+      (Name id, Some j.uj_val, j.uj_type)
   | LocalAssum c ->
-      let (j,cst) = infer env c in
-      (Name id, None, assumption_of_judgment env j), cst
+      let j = infer env c in
+      (Name id, None, assumption_of_judgment env j)
 
 let infer_local_decls env decls =
   let rec inferec env = function
   | (id, d) :: l ->
-      let env, l, cst1 = inferec env l in
-      let d, cst2 = infer_local_decl env id d in
-      push_rel d env, add_rel_decl d l, union_constraints cst1 cst2
-  | [] -> env, empty_rel_context, empty_constraint in
+      let (env, l) = inferec env l in
+      let d = infer_local_decl env id d in
+	(push_rel d env, add_rel_decl d l)
+  | [] -> (env, empty_rel_context) in
   inferec env decls
-
-(* Exported typing functions *)
-
-let typing env c =
-  let (j,cst) = infer env c in
-  let _ = add_constraints cst env in
-  j