Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from

svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses

........
  r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Comment grammar error
........
  r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
  
  The initial Type Classes patch.
  This patch introduces type classes and instance definitions a la Haskell.
  Technically, it uses the implicit arguments mechanism which was extended a bit. 
  The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
  It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). 
........
  r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix interface
........
  r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix more xlate code
........
  r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
  r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Bug fixes in Instance decls.
........
  r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
  
  Streamline typeclass context implementation, prepare for class binders in proof statements.
........
  r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
  
  Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
  r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
  
  Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
  r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
  
  Stupid bug
........
  r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
  r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
  r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
  
  Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
  New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
  Other bugs related to naming in typeclasses fixed. 
........
  r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
  
  Progress on setoids using type classes, recognize setoid equalities in hyps better.
  Streamline implementation to return more information when resolving setoids (return the results setoid).
........
  r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
  
  Syntax change, more like Coq
........
  r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
  
  Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
  r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
  
  Work on type classes based rewrite tactic.
........
  r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
  
  Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
  r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
  
  Forgot to add a file
........
  r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
  
  Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and 
  implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
  r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
  
  Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. 
  Add useful tactics to Program.Subsets.
........


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 67 insertions, 59 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 612be05e3..97f7c1d97 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -139,8 +139,8 @@ type newfixpoint_expr =
 let rec abstract_rawconstr c = function
   | [] -> c
   | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
-  | Topconstr.LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl
+  | Topconstr.LocalRawAssum (idl,k,t)::bl ->
+      List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
         (abstract_rawconstr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
@@ -213,7 +213,7 @@ let rec is_rec names =
     | RRec _ -> error "RRec not handled"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b)  -> 
+    | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b)  -> 
 	lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
     | RLetTuple(_,nal,_,t,b) -> lookup names t || 
 	lookup 
@@ -434,7 +434,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
       | None -> 
 	  begin
 	    match args with 
-	      | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x 
+	      | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x 
 	      | _ -> error "Recursive argument must be specified" 
 	  end
       | Some wf_args -> 
@@ -442,7 +442,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
 	    match 
 	      List.find 
 		(function 
-		   | Topconstr.LocalRawAssum(l,t) -> 
+		   | Topconstr.LocalRawAssum(l,k,t) -> 
 		       List.exists 
 			 (function (_,Name id) -> id =  wf_args | _ -> false) 
 			 l 
@@ -450,7 +450,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
 		)
 		args 
 	    with 
-	      | Topconstr.LocalRawAssum(_,t)  ->	    t,wf_args
+	      | Topconstr.LocalRawAssum(_,k,t)  ->	    t,wf_args
 	      | _ -> assert false 
 	  with Not_found -> assert false 
   in
@@ -462,7 +462,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
   let fun_from_mes = 
     let applied_mes = 
       Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg])    in
-    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes) 
+    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) 
   in
   let wf_rel_from_mes = 
     Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
@@ -570,11 +570,11 @@ let rec add_args id new_args b =
       CArrow(loc,add_args id new_args  b1, add_args id new_args b2)
   | CProdN(loc,nal,b1) -> 
       CProdN(loc,
-	     List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, 
+	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, 
 	     add_args id new_args  b1)
   | CLambdaN(loc,nal,b1) -> 
       CLambdaN(loc,
-	       List.map (fun (nal,b2) -> (nal,add_args id new_args  b2)) nal, 
+	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal, 
 	       add_args id new_args  b1)
   | CLetIn(loc,na,b1,b2) -> 
       CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
@@ -644,13 +644,15 @@ let rec chop_n_arrow n t =
 	      let new_n =
 		let rec aux (n:int) = function 
 		    [] -> n
-		| (nal,t'')::nal_ta' -> 
+		| (nal,k,t'')::nal_ta' -> 
 		    let nal_l = List.length nal in 
 		    if n >= nal_l
 		    then 
 		      aux (n - nal_l) nal_ta'
 		    else 
-		      let new_t' = Topconstr.CProdN(dummy_loc,((snd (list_chop n nal)),t'')::nal_ta',t')
+		      let new_t' = 
+			Topconstr.CProdN(dummy_loc,
+					((snd (list_chop n nal)),k,t'')::nal_ta',t')
 		      in 
 		      raise (Stop new_t')
 		in
@@ -668,12 +670,12 @@ let rec get_args b t : Topconstr.local_binder list *
     | Topconstr.CLambdaN (loc, (nal_ta), b') -> 
 	begin
 	  let n = 
-	    (List.fold_left (fun n (nal,_) -> 
+	    (List.fold_left (fun n (nal,_,_) -> 
 			       n+List.length nal) 0 nal_ta )
 	  in
 	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in 
-	  (List.map (fun (nal,ta) -> 
-		       (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' 
+	  (List.map (fun (nal,k,ta) -> 
+		       (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' 
 	end
     | _ -> [],b,t
 
@@ -716,7 +718,7 @@ let make_graph (f_ref:global_reference) =
 			   (List.map 
 			      (function 
 				 | Topconstr.LocalRawDef (na,_)-> []
-				 | Topconstr.LocalRawAssum (nal,_) -> nal
+				 | Topconstr.LocalRawAssum (nal,_,_) -> nal
 			      )
 			      bl
 			   )
@@ -730,7 +732,7 @@ let make_graph (f_ref:global_reference) =
 			   (List.map 
 			      (function
  				 | Topconstr.LocalRawDef (na,_)-> []
-			      	 | Topconstr.LocalRawAssum (nal,_) -> 
+			      	 | Topconstr.LocalRawAssum (nal,_,_) -> 
 				     List.map 
 				       (fun (loc,n) -> 
 					  CRef(Libnames.Ident(loc, Nameops.out_name n))) 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 5ad4632e4..78e2c4408 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -76,7 +76,7 @@ let chop_rlambda_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
+	  | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
 	  | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ -> 
 	      raise (Util.UserError("chop_rlambda_n",
@@ -90,7 +90,7 @@ let chop_rprod_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+	  | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
 	  | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index b6398a329..4b3492b12 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -148,7 +148,7 @@ END
 VERNAC ARGUMENT EXTEND binder2
     [ "(" ne_ident_list(idl) ":" lconstr(c)  ")"] ->
      [
-       LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ]
+       LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ]
 END
 
 
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 44df08598..adec67e36 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -830,7 +830,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let _ = prNamedRConstr (string_of_name nme) tp in
         let _ = prstr "  ;  " in
         let typ = rawterm_to_constr_expr tp in
-        LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc)
+        LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc)
       [] params in
   let concl = Constrextern.extern_constr false (Global.env()) concl in
   let arity,_ = 
@@ -838,7 +838,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
       (fun (acc,env) (nm,_,c) -> 
         let typ = Constrextern.extern_constr false env c in
         let newenv = Environ.push_rel (nm,None,c) env in
-        CProdN (dummy_loc, [[(dummy_loc,nm)],typ] , acc) , newenv)
+        CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1 
         @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in  
@@ -867,7 +867,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
   match rdecl with
     | (nme,None,t) -> 
         let traw = Detyping.detype false [] [] t in
-        RProd (dummy_loc,nme,traw,t2)
+        RProd (dummy_loc,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
@@ -877,7 +877,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
   match rdecl with
     | (nme,None,t) -> 
         let traw = Detyping.detype false [] [] t in
-        RProd (dummy_loc,nme,traw,t2)
+        RProd (dummy_loc,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 2f6f5914d..9bea4f1e0 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -586,7 +586,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	    | RProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *) 
 
-    | RLambda(_,n,t,b) ->
+    | RLambda(_,n,_,t,b) ->
 	(* we first compute the list of constructor 
 	   corresponding to the body of the function, 
 	   then the one corresponding to the type 
@@ -601,7 +601,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	let new_env = raw_push_named (new_n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_lam new_n) t_res b_res
-    | RProd(_,n,t,b) ->
+    | RProd(_,n,_,t,b) ->
 	(* we first compute the list of constructor 
 	   corresponding to the body of the function, 
 	   then the one corresponding to the type 
@@ -865,7 +865,7 @@ let is_res id =
 *)
 let rec rebuild_cons nb_args relname args crossed_types depth rt = 
   match rt with 
-    | RProd(_,n,t,b) -> 
+    | RProd(_,n,k,t,b) -> 
 	let not_free_in_t id = not (is_free_in id t) in 
 	let new_crossed_types = t::crossed_types in 
 	begin
@@ -928,7 +928,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 			(Idset.filter not_free_in_t id_to_exclude)
 		  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	end
-    | RLambda(_,n,t,b) ->
+    | RLambda(_,n,k,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
@@ -944,7 +944,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 		then 
 		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
 		else
-		  RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  RProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly "Should not have an anonymous function here" 
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 	  
@@ -1016,7 +1016,7 @@ let rec compute_cst_params relnames params = function
       compute_cst_params_from_app [] (params,rtl)
   | RApp(_,f,args) -> 
       List.fold_left (compute_cst_params relnames) params (f::args)
-  | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
+  | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
       let t_params = compute_cst_params relnames params t in 
       compute_cst_params relnames t_params b
   | RCases _ -> params  (* If there is still cases at this point they can only be 
@@ -1153,7 +1153,7 @@ let do_build_inductive
 	 else
 	   Topconstr.CProdN
 	   (dummy_loc,
-	    [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t],
+	   [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
 	    acc
 	   )
       )
@@ -1173,7 +1173,7 @@ let do_build_inductive
 	   Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t)
 	 else
 	 Topconstr.LocalRawAssum 
-	   ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t)
+	   ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t)
       )
       rels_params
   in 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index e8cce47ad..0c03c1e61 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -12,8 +12,8 @@ let idmap_is_empty m = m = Idmap.empty
 let mkRRef ref = RRef(dummy_loc,ref)
 let mkRVar id = RVar(dummy_loc,id)
 let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
-let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b)
-let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b)
+let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
+let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
 let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
 let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
@@ -26,7 +26,7 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
 *)
 let raw_decompose_prod = 
   let rec raw_decompose_prod args = function 
-  | RProd(_,n,t,b) -> 
+  | RProd(_,n,k,t,b) -> 
       raw_decompose_prod ((n,t)::args) b 
   | rt -> args,rt
   in
@@ -34,7 +34,7 @@ let raw_decompose_prod =
 
 let raw_decompose_prod_or_letin = 
   let rec raw_decompose_prod args = function 
-  | RProd(_,n,t,b) -> 
+  | RProd(_,n,k,t,b) -> 
       raw_decompose_prod ((n,None,Some t)::args) b 
   | RLetIn(_,n,t,b) -> 
       raw_decompose_prod ((n,Some t,None)::args) b 
@@ -58,7 +58,7 @@ let raw_decompose_prod_n n =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,t,b) -> 
+	| RProd(_,n,_,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,t)::args) b 
 	| rt -> args,rt
   in
@@ -70,7 +70,7 @@ let raw_decompose_prod_or_letin_n n =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,t,b) -> 
+	| RProd(_,n,_,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,None,Some t)::args) b 
 	| RLetIn(_,n,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,Some t,None)::args) b 
@@ -135,15 +135,17 @@ let change_vars =
 	       change_vars mapping rt',
 	       List.map (change_vars mapping) rtl
 	      )
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | RProd(loc,name,t,b) -> 
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
 		  name,
+	          k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
@@ -261,21 +263,21 @@ let rec alpha_rt excluded rt =
   let new_rt = 
     match rt with   
       | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
-      | RLambda(loc,Anonymous,t,b) -> 
+      | RLambda(loc,Anonymous,k,t,b) -> 
 	  let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in 
 	  let new_excluded = new_id :: excluded in 
 	  let new_t = alpha_rt new_excluded t in 
 	  let new_b = alpha_rt new_excluded b in 
-	  RLambda(loc,Name new_id,new_t,new_b)
-      | RProd(loc,Anonymous,t,b) -> 
+	  RLambda(loc,Name new_id,k,new_t,new_b)
+      | RProd(loc,Anonymous,k,t,b) -> 
 	let new_t = alpha_rt excluded t in 
 	let new_b = alpha_rt excluded b in 
-	RProd(loc,Anonymous,new_t,new_b)
+	RProd(loc,Anonymous,k,new_t,new_b)
     | RLetIn(loc,Anonymous,t,b) -> 
 	let new_t = alpha_rt excluded t in 
 	let new_b = alpha_rt excluded b in 
 	RLetIn(loc,Anonymous,new_t,new_b)
-    | RLambda(loc,Name id,t,b) -> 
+    | RLambda(loc,Name id,k,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let t,b = 
 	  if new_id = id 
@@ -287,8 +289,8 @@ let rec alpha_rt excluded rt =
 	let new_excluded = new_id::excluded in 
 	let new_t = alpha_rt new_excluded t in 
 	let new_b = alpha_rt new_excluded b in 
-	RLambda(loc,Name new_id,new_t,new_b)
-    | RProd(loc,Name id,t,b) -> 
+	RLambda(loc,Name new_id,k,new_t,new_b)
+    | RProd(loc,Name id,k,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let new_excluded = new_id::excluded in 
 	let t,b = 
@@ -300,7 +302,7 @@ let rec alpha_rt excluded rt =
 	in
 	let new_t = alpha_rt new_excluded t in 
 	let new_b = alpha_rt new_excluded b in 
-	RProd(loc,Name new_id,new_t,new_b)
+	RProd(loc,Name new_id,k,new_t,new_b)
     | RLetIn(loc,Name id,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let t,b = 
@@ -389,7 +391,7 @@ let is_free_in id =
     | REvar _ -> false
     | RPatVar _ -> false
     | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
-    | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) ->
+    | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) ->
 	let check_in_b =
 	  match n with
 	    | Name id' -> id_ord id' id <> 0
@@ -460,17 +462,19 @@ let replace_var_by_term x_id term =
 	       replace_var_by_pattern rt',
 	       List.map replace_var_by_pattern rtl
 	      )
-      | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt
-      | RProd(loc,name,t,b) -> 
+      | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
 		  name,
+	          k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
@@ -590,8 +594,8 @@ let ids_of_rawterm c =
       | RVar (_,id) -> id::acc
       | RApp (loc,g,args) -> 
           ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
-      | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
-      | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
       | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
       | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
       | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
@@ -622,15 +626,17 @@ let zeta_normalize =
 	       zeta_normalize_term rt',
 	       List.map zeta_normalize_term rtl
 	      )
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  zeta_normalize_term t,
 		  zeta_normalize_term b
 		 )
-      | RProd(loc,name,t,b) -> 
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
-		name, 		  
+		name, 		
+	        k,
 		zeta_normalize_term t,
 		zeta_normalize_term b
 		 )
@@ -691,8 +697,8 @@ let expand_as =
 	    with Not_found -> rt 
 	  end
       | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
-      | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b)
-      | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
+      | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b)
+      | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b)
       | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
       | RLetTuple(loc,nal,(na,po),v,b) ->
 	  RLetTuple(loc,nal,(na,Option.map (expand_as map) po),