Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

10 files changed, 217 insertions, 209 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6442cb94..daa57b77 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 8675 2006-03-31 18:21:20Z herbelin $ *)
+(* $Id: constrextern.ml 8831 2006-05-19 09:29:54Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -27,6 +27,7 @@ open Pattern
 open Nametab
 open Notation
 open Reserve
+open Detyping
 (*i*)
 
 (* Translation from rawconstr to front constr *)
@@ -259,7 +260,7 @@ let rec same_raw c d =
         (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
           same_raw t1 t2;
           if al1 <> al2 then failwith "RCases";
-          option_iter2(fun (_,i1,nl1) (_,i2,nl2) ->
+          option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
             if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
       List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
         List.iter2 same_patt pl1 pl2;
@@ -622,6 +623,11 @@ let extern_optimal_prim_token scopes r r' =
 (**********************************************************************)
 (* mapping rawterms to constr_expr                                    *)
 
+let extern_rawsort = function
+  | RProp _ as s -> s
+  | RType (Some _) as s when !print_universes -> s
+  | RType _ -> RType None
+
 let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
   try 
@@ -679,7 +685,7 @@ let rec extern inctx scopes vars r =
       let vars' = 
 	List.fold_right (name_fold Idset.add)
 	  (cases_predicate_names tml) vars in
-      let rtntypopt' = option_app (extern_typ scopes vars') rtntypopt in
+      let rtntypopt' = option_map (extern_typ scopes vars') rtntypopt in
       let tml = List.map (fun (tm,(na,x)) ->
         let na' = match na,tm with
             Anonymous, RVar (_,id) when 
@@ -689,26 +695,28 @@ let rec extern inctx scopes vars r =
           | Name id, RVar (_,id') when id=id' -> None
           | Name _, _ -> Some na in
 	(sub_extern false scopes vars tm,
-	(na',option_app (fun (loc,ind,nal) ->
+	(na',option_map (fun (loc,ind,n,nal) ->
+	  let params = list_tabulate
+	    (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
 	  let args = List.map (function
 	    | Anonymous -> RHole (dummy_loc,Evd.InternalHole) 
 	    | Name id -> RVar (dummy_loc,id)) nal in
-	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in
+	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
 	  (extern_typ scopes vars t)) x))) tml in
       let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in 
       CCases (loc,rtntypopt',tml,eqns)
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
-        (option_app (fun _ -> na) typopt,
-         option_app (extern_typ scopes (add_vname vars na)) typopt),
+        (option_map (fun _ -> na) typopt,
+         option_map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (option_app (fun _ -> na) typopt,
-         option_app (extern_typ scopes (add_vname vars na)) typopt),
+        (option_map (fun _ -> na) typopt,
+         option_map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
   | RRec (loc,fk,idv,blv,tyv,bv) ->
@@ -737,12 +745,7 @@ let rec extern inctx scopes vars r =
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
-  | RSort (loc,s) ->
-      let s = match s with
-	 | RProp _ -> s
-	 | RType (Some _) when !print_universes -> s
-	 | RType _ -> RType None in
-      CSort (loc,s)
+  | RSort (loc,s) -> CSort (loc,extern_rawsort s)
 
   | RHole (loc,e) -> CHole loc
 
@@ -870,9 +873,18 @@ let extern_type at_top env t =
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   extern_rawtype (vars_of_env env) r
 
+let extern_sort s = extern_rawsort (detype_sort s)
+
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
+let it_destPLambda n c =
+  let rec aux n nal c =
+    if n=0 then (nal,c) else match c with
+      | PLambda (na,_,c) -> aux (n-1) (na::nal) c
+      | _ -> anomaly "it_destPLambda" in
+  aux n [] c
+
 let rec raw_of_pat env = function
   | PRef ref -> RRef (loc,ref)
   | PVar id -> RVar (loc,id)
@@ -897,20 +909,24 @@ let rec raw_of_pat env = function
       RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
   | PLambda (na,t,c) ->
       RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
-  | PCase ((_,cs),typopt,tm,[||]) ->
-      if typopt <> None then failwith "TODO: PCase to RCases";
-      RCases (loc,(*(option_app (raw_of_pat env) typopt,*)None,
-         [raw_of_pat env tm,(Anonymous,None)],[])
-  | PCase ((Some ind,cs),typopt,tm,bv) ->
-      let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
-      let mib,mip = lookup_mind_specif (Global.env()) ind in
-      let k = mip.Declarations.mind_nrealargs in
-      let nparams = mib.Declarations.mind_nparams in
-      let cstrnargs = mip.Declarations.mind_consnrealdecls in
-      Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env)
-	(fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
-	avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv
-  | PCase _ -> error "Unsupported case-analysis while printing pattern"
+  | PIf (c,b1,b2) ->
+      RIf (loc, raw_of_pat env c, (Anonymous,None), 
+           raw_of_pat env b1, raw_of_pat env b2)
+  | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
+      let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
+      RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
+  | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
+      let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
+      let brns = Array.to_list cstr_nargs in
+        (* ind is None only if no branch and no return type *)
+      let ind = out_some indo in
+      let mat = simple_cases_matrix_of_branches ind brns brs in
+      let indnames,rtn =
+	if p = PMeta None then (Anonymous,None),None
+	else 
+	  let nparams,n = out_some ind_nargs in
+	  return_type_of_predicate ind nparams n (raw_of_pat env p) in
+      RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 1fc44250..ca145dd9 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrextern.mli 7837 2006-01-11 09:47:32Z herbelin $ i*)
+(*i $Id: constrextern.mli 8831 2006-05-19 09:29:54Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -41,6 +41,7 @@ val extern_constr : bool -> env -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
 val extern_reference : loc -> Idset.t -> global_reference -> reference
 val extern_type : bool -> env -> types -> constr_expr
+val extern_sort : sorts -> rawsort
 
 (* Printing options *)
 val print_implicits : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6fcd9d7a..678fb87b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 8654 2006-03-22 15:36:58Z msozeau $ *)
+(* $Id: constrintern.ml 8924 2006-06-08 17:49:01Z notin $ *)
 
 open Pp
 open Util
@@ -22,6 +22,7 @@ open Cases
 open Topconstr
 open Nametab
 open Notation
+open Inductiveops
 
 (* To interpret implicits and arg scopes of recursive variables in
    inductive types and recursive definitions *)
@@ -38,8 +39,8 @@ let interning_grammar = ref false
 let for_grammar f x =
   interning_grammar := true;
   let a = f x in
-  interning_grammar := false;
-  a
+    interning_grammar := false;
+    a
 
 let variables_bind = ref false
 
@@ -128,9 +129,9 @@ type coqdoc_state = Lexer.location_table * int * int
 let coqdoc_freeze () =
   let lt = Lexer.location_table() in
   let state = (lt,!token_number,!last_pos) in
-  token_number := 0;
-  last_pos := 0;
-  state
+    token_number := 0;
+    last_pos := 0;
+    state
 
 let coqdoc_unfreeze (lt,tn,lp) =
   Lexer.restore_location_table lt;
@@ -138,21 +139,13 @@ let coqdoc_unfreeze (lt,tn,lp) =
   last_pos := lp
 
 let add_glob loc ref = 
-(*i
-  let sp = Nametab.sp_of_global (Global.env ()) ref in
-  let dir,_ = repr_path sp in
-  let rec find_module d = 
-    try 
-      let qid = let dir,id = split_dirpath d in make_qualid dir id in
-      let _ = Nametab.locate_loaded_library qid in d
-    with Not_found -> find_module (dirpath_prefix d) 
-  in
-  let s = string_of_dirpath (find_module dir) in
-  i*)
   let sp = Nametab.sp_of_global ref in
-  let id = let _,id = repr_path sp in string_of_id id in
-  let dp = string_of_dirpath (Lib.library_part ref) in
-  dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id)
+  let lib_dp = Lib.library_part ref in
+  let mod_dp,id = repr_path sp in
+  let mod_dp_trunc =  drop_dirpath_prefix lib_dp mod_dp in
+  let filepath = string_of_dirpath lib_dp in
+  let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in
+    dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname)
 
 let loc_of_notation f loc args ntn =
   if args=[] or ntn.[0] <> '_' then fst (unloc loc)
@@ -165,15 +158,15 @@ let dump_notation_location pos ((path,df),sc) =
   let rec next growing =
     let loc = Lexer.location_function !token_number in
     let (bp,_) = unloc loc in
-    if growing then if bp >= pos then loc else (incr token_number;next true)
-    else if bp = pos then loc
-    else if bp > pos then (decr token_number;next false)
-    else (incr token_number;next true) in
+      if growing then if bp >= pos then loc else (incr token_number;next true)
+      else if bp = pos then loc
+      else if bp > pos then (decr token_number;next false)
+      else (incr token_number;next true) in
   let loc = next (pos >= !last_pos) in
-  last_pos := pos;
-  let path = string_of_dirpath path in
-  let sc = match sc with Some sc -> " "^sc | None -> "" in
-  dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
+    last_pos := pos;
+    let path = string_of_dirpath path in
+    let sc = match sc with Some sc -> " "^sc | None -> "" in
+      dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -390,11 +383,6 @@ let check_constructor_length env loc cstr pl pl0 =
   if n <> nargs && n <> nhyps (* i.e. with let's *) then
     error_wrong_numarg_constructor_loc loc env cstr nargs
 
-let check_inductive_length env (loc,ind,nal) =
-  let n = Inductiveops.inductive_nargs env ind in
-  if n <> List.length nal then
-    error_wrong_numarg_inductive_loc loc env ind n
-
 (* Manage multiple aliases *)
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
@@ -506,20 +494,20 @@ let find_constructor ref =
     try extended_locate qid
     with Not_found ->
       raise (InternalisationError (loc,NotAConstructor ref)) in
-  match gref with
-    | SyntacticDef sp ->
-        let sdef = Syntax_def.search_syntactic_definition loc sp in
-        patt_of_rawterm loc sdef
-    | TrueGlobal r ->
-        let rec unf = function
-          | ConstRef cst ->
-	      let v = Environ.constant_value (Global.env()) cst in
-              unf (global_of_constr v)
-          | ConstructRef c -> 
-	      if !dump then add_glob loc r; 
-	      c, []
-          | _ -> raise Not_found
-        in unf r
+    match gref with
+      | SyntacticDef sp ->
+          let sdef = Syntax_def.search_syntactic_definition loc sp in
+            patt_of_rawterm loc sdef
+      | TrueGlobal r ->
+          let rec unf = function
+            | ConstRef cst ->
+		let v = Environ.constant_value (Global.env()) cst in
+		  unf (global_of_constr v)
+            | ConstructRef c -> 
+		if !dump then add_glob loc r; 
+		c, []
+            | _ -> raise Not_found
+          in unf r
 
 let find_pattern_variable = function
   | Ident (loc,id) -> id
@@ -793,7 +781,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
 		     RStructRec,
 		     List.fold_left intern_local_binder (env,[]) bl
 		 | CWfRec c -> 
-		     let before, after = list_chop (succ n) bl in
+		     let before, after = list_chop (succ (out_some n)) bl in
 		     let ((ids',_,_),rafter) =
 		       List.fold_left intern_local_binder (env,[]) after in
 		     let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
@@ -887,21 +875,21 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	    let (tm,ind),nal = intern_case_item env citm in
 	    (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
 	  tms ([],env) in
-        let rtnpo = option_app (intern_type env') rtnpo in
+        let rtnpo = option_map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	RCases (loc, rtnpo, tms, List.flatten eqns')
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
         let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_app (intern_type env'') po in
+        let p' = option_map (intern_type env'') po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
         let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_app (intern_type env'') po in
+        let p' = option_map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
 	RHole (loc, Evd.QuestionMark)
@@ -958,18 +946,25 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	let tids = names_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
 	let t = intern_type (tids,None,scopes) t in
-	let (_,_,nal as indsign) =
+	let (_,_,_,nal as indsign) =
 	  match t with
-	  | RRef (loc,IndRef ind) -> (loc,ind,[])
+	  | RRef (loc,IndRef ind) -> (loc,ind,0,[])
 	  | RApp (loc,RRef (_,IndRef ind),l) ->
+	      let nparams, nrealargs = inductive_nargs globalenv ind in
+	      let nindargs = nparams + nrealargs in
+	      if List.length l <> nindargs then
+		error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
 	      let nal = List.map (function
 		| RHole _ -> Anonymous
 		| RVar (_,id) -> Name id
 		| c ->
 		    user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
-	      (loc,ind,nal)
+	      let parnal,realnal = list_chop nparams nal in
+	      if List.exists ((<>) Anonymous) parnal then
+		user_err_loc (loc,"",
+		  str "The parameters of inductive type must be implicit");
+	      (loc,ind,nparams,realnal)
 	  | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
-	check_inductive_length globalenv indsign;
 	nal, Some indsign
     | None -> 
 	[], None in
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index afee83e8..79a217a1 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqlib.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: coqlib.ml 8866 2006-05-28 16:21:04Z herbelin $ *)
 
 open Util
 open Pp
@@ -152,12 +152,7 @@ type coq_sigma_data = {
 
 type 'a delayed = unit -> 'a
 
-let build_sigma_set () =
-  { proj1 = init_constant ["Specif"] "projS1";
-    proj2 = init_constant ["Specif"] "projS2";
-    elim = init_constant ["Specif"] "sigS_rec";
-    intro = init_constant ["Specif"] "existS";
-    typ = init_constant ["Specif"] "sigS" }
+let build_sigma_set () = anomaly "Use build_sigma_type"
 
 let build_sigma_type () =
   { proj1 = init_constant ["Specif"] "projT1";
@@ -257,7 +252,7 @@ let build_coq_ex ()   = Lazy.force coq_ex
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
 let coq_identity_ref     = lazy (init_reference ["Datatypes"] "identity")
-let coq_existS_ref  = lazy (init_reference ["Specif"] "existS")
+let coq_existS_ref  = lazy (anomaly "use coq_existT_ref")
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
 let coq_False_ref   = lazy (init_reference ["Logic"] "False")
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 511cf88a..77ed1fe6 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: genarg.ml 7879 2006-01-16 13:58:09Z herbelin $ *)
+(* $Id: genarg.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
 
 open Pp
 open Util
@@ -33,7 +33,6 @@ type argument_type =
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
-  | TacticArgType of int
   | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
@@ -44,7 +43,6 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
-type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a and_short_name = 'a * identifier located option
 type rawconstr_and_expr = rawconstr * constr_expr option
 
@@ -54,6 +52,10 @@ type ('a,'b) generic_argument = argument_type * Obj.t
 
 let dyntab = ref ([] : string list)
 
+type rlevel = constr_expr
+type glevel = rawconstr_and_expr
+type tlevel = constr
+
 type ('a,'b,'c) abstract_argument_type = argument_type
 
 let create_arg s =
@@ -142,10 +144,6 @@ let rawwit_constr_may_eval = ConstrMayEvalArgType
 let globwit_constr_may_eval = ConstrMayEvalArgType
 let wit_constr_may_eval = ConstrMayEvalArgType
 
-let rawwit_tactic n = TacticArgType n
-let globwit_tactic n = TacticArgType n
-let wit_tactic n = TacticArgType n
-
 let rawwit_open_constr_gen b = OpenConstrArgType b
 let globwit_open_constr_gen b = OpenConstrArgType b 
 let wit_open_constr_gen b = OpenConstrArgType b
@@ -220,7 +218,7 @@ let app_list1 f = function
 let app_opt f = function
   | (OptArgType t as u, l) ->
       let o = Obj.magic l in
-      (u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o))
+      (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o))
   | _ -> failwith "Genarg: not an opt"
 
 let app_pair f1 f2 = function
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 99de4ca4..37b30927 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: genarg.mli 7879 2006-01-16 13:58:09Z herbelin $ i*)
+(*i $Id: genarg.mli 8926 2006-06-08 20:23:17Z herbelin $ i*)
 
 open Util
 open Names
@@ -16,7 +16,6 @@ open Rawterm
 open Topconstr
 open Term
 
-type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a and_short_name = 'a * identifier located option
 
 (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
@@ -73,7 +72,6 @@ RefArgType                     reference                global_reference
 ConstrArgType                  constr_expr              constr
 ConstrMayEvalArgType           constr_expr may_eval     constr
 QuantHypArgType                quantified_hypothesis    quantified_hypothesis
-TacticArgType                  raw_tactic_expr          tactic
 OpenConstrArgType              constr_expr              open_constr
 ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
 List0ArgType of argument_type
@@ -83,88 +81,94 @@ ExtraArgType of string         '_a                      '_b
 \end{verbatim}
 *)
 
-type ('a,'co,'ta) abstract_argument_type
+(* All of [rlevel], [glevel] and [tlevel] must be non convertible 
+   to ensure the injectivity of the type inference from type
+   [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type]
+   is injective; this guarantees that, for 'b fixed, the type of
+   out_gen is monomorphic over 'a, hence type-safe 
+*)
 
-val rawwit_bool : (bool,'co,'ta) abstract_argument_type
-val globwit_bool : (bool,'co,'ta) abstract_argument_type
-val wit_bool : (bool,'co,'ta) abstract_argument_type
+type rlevel = constr_expr
+type glevel = rawconstr_and_expr
+type tlevel = constr
+
+type ('a,'co,'ta) abstract_argument_type
 
-val rawwit_int : (int,'co,'ta) abstract_argument_type
-val globwit_int : (int,'co,'ta) abstract_argument_type
-val wit_int : (int,'co,'ta) abstract_argument_type
+val rawwit_bool : (bool,rlevel,'ta) abstract_argument_type
+val globwit_bool : (bool,glevel,'ta) abstract_argument_type
+val wit_bool : (bool,tlevel,'ta) abstract_argument_type
 
-val rawwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
-val globwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
-val wit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
+val rawwit_int : (int,rlevel,'ta) abstract_argument_type
+val globwit_int : (int,glevel,'ta) abstract_argument_type
+val wit_int : (int,tlevel,'ta) abstract_argument_type
 
-val rawwit_string : (string,'co,'ta) abstract_argument_type
-val globwit_string : (string,'co,'ta) abstract_argument_type
-val wit_string : (string,'co,'ta) abstract_argument_type
+val rawwit_int_or_var : (int or_var,rlevel,'ta) abstract_argument_type
+val globwit_int_or_var : (int or_var,glevel,'ta) abstract_argument_type
+val wit_int_or_var : (int or_var,tlevel,'ta) abstract_argument_type
 
-val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type
-val globwit_pre_ident : (string,'co,'ta) abstract_argument_type
-val wit_pre_ident : (string,'co,'ta) abstract_argument_type
+val rawwit_string : (string,rlevel,'ta) abstract_argument_type
+val globwit_string : (string,glevel,'ta) abstract_argument_type
+val wit_string : (string,tlevel,'ta) abstract_argument_type
 
-val rawwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
-val globwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
-val wit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+val rawwit_pre_ident : (string,rlevel,'ta) abstract_argument_type
+val globwit_pre_ident : (string,glevel,'ta) abstract_argument_type
+val wit_pre_ident : (string,tlevel,'ta) abstract_argument_type
 
-val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
-val globwit_ident : (identifier,'co,'ta) abstract_argument_type
-val wit_ident : (identifier,'co,'ta) abstract_argument_type
+val rawwit_intro_pattern : (intro_pattern_expr,rlevel,'ta) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr,glevel,'ta) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr,tlevel,'ta) abstract_argument_type
 
-val rawwit_var : (identifier located,'co,'ta) abstract_argument_type
-val globwit_var : (identifier located,'co,'ta) abstract_argument_type
-val wit_var : (identifier,'co,'ta) abstract_argument_type
+val rawwit_ident : (identifier,rlevel,'ta) abstract_argument_type
+val globwit_ident : (identifier,glevel,'ta) abstract_argument_type
+val wit_ident : (identifier,tlevel,'ta) abstract_argument_type
 
-val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
-val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_ref : (global_reference,constr,'ta) abstract_argument_type
+val rawwit_var : (identifier located,rlevel,'ta) abstract_argument_type
+val globwit_var : (identifier located,glevel,'ta) abstract_argument_type
+val wit_var : (identifier,tlevel,'ta) abstract_argument_type
 
-val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
-val globwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
-val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
+val rawwit_ref : (reference,rlevel,'ta) abstract_argument_type
+val globwit_ref : (global_reference located or_var,glevel,'ta) abstract_argument_type
+val wit_ref : (global_reference,tlevel,'ta) abstract_argument_type
 
-val rawwit_sort : (rawsort,constr_expr,'ta) abstract_argument_type
-val globwit_sort : (rawsort,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_sort : (sorts,constr,'ta) abstract_argument_type
+val rawwit_quant_hyp : (quantified_hypothesis,rlevel,'ta) abstract_argument_type
+val globwit_quant_hyp : (quantified_hypothesis,glevel,'ta) abstract_argument_type
+val wit_quant_hyp : (quantified_hypothesis,tlevel,'ta) abstract_argument_type
 
-val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_constr : (rawconstr_and_expr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_constr : (constr,constr,'ta) abstract_argument_type
+val rawwit_sort : (rawsort,rlevel,'ta) abstract_argument_type
+val globwit_sort : (rawsort,glevel,'ta) abstract_argument_type
+val wit_sort : (sorts,tlevel,'ta) abstract_argument_type
 
-val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
+val rawwit_constr : (constr_expr,rlevel,'ta) abstract_argument_type
+val globwit_constr : (rawconstr_and_expr,glevel,'ta) abstract_argument_type
+val wit_constr : (constr,tlevel,'ta) abstract_argument_type
 
-val rawwit_open_constr_gen : bool -> (open_constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_open_constr_gen : bool -> (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_open_constr_gen : bool -> (open_constr,constr,'ta) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel,'ta) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel,'ta) abstract_argument_type
+val wit_constr_may_eval : (constr,tlevel,'ta) abstract_argument_type
 
-val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type
+val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel,'ta) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_rawconstr,glevel,'ta) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr,tlevel,'ta) abstract_argument_type
 
-val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type
+val rawwit_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
+val globwit_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
+val wit_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
 
-val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type
-val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
+val rawwit_casted_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
+val wit_casted_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
 
-val rawwit_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type
-val globwit_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_bindings : (constr bindings,constr,'ta) abstract_argument_type
+val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel,'ta) abstract_argument_type
+val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel,'ta) abstract_argument_type
+val wit_constr_with_bindings : (constr with_bindings,tlevel,'ta) abstract_argument_type
 
-val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
+val rawwit_bindings : (constr_expr bindings,rlevel,'ta) abstract_argument_type
+val globwit_bindings : (rawconstr_and_expr bindings,glevel,'ta) abstract_argument_type
+val wit_bindings : (constr bindings,tlevel,'ta) abstract_argument_type
 
-(* TODO: transformer tactic en extra arg *)
-val rawwit_tactic : int -> ('ta,constr_expr,'ta) abstract_argument_type
-val globwit_tactic : int -> ('ta,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_tactic : int -> ('ta,constr,'ta) abstract_argument_type
+val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel,'ta) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel,'ta) abstract_argument_type
+val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel,'ta) abstract_argument_type
 
 val wit_list0 :
   ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
@@ -217,9 +221,9 @@ val app_pair :
    polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
    de create *)
 val create_arg : string ->
-      ('a,'co,'ta) abstract_argument_type
-      * ('globa,'globco,'globta) abstract_argument_type
-      * ('rawa,'rawco,'rawta) abstract_argument_type
+      ('a,tlevel,'ta) abstract_argument_type
+      * ('globa,glevel,'globta) abstract_argument_type
+      * ('rawa,rlevel,'rawta) abstract_argument_type
 
 val exists_argtype : string -> bool
 
@@ -239,7 +243,6 @@ type argument_type =
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
-  | TacticArgType of int
   | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
diff --git a/interp/notation.ml b/interp/notation.ml
index cb996dfe..7e101784 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 7984 2006-02-04 20:14:55Z herbelin $ *)
+(* $Id: notation.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 (*i*)
 open Util
@@ -234,12 +234,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
-    (patl, (fun r -> option_app mkNumeral (uninterp r)), inpat)
+    (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> option_app mkString (uninterp r)), inpat)
+    (patl, (fun r -> option_map mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.absolute_reference sp in ()
@@ -389,7 +389,7 @@ let uninterp_prim_token_cases_pattern c =
 
 let availability_of_prim_token printer_scope scopes =
   let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
-  option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
+  option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 476fd7e6..aee981bd 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reserve.ml 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: reserve.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
 
 (* Reserved names *)
 
@@ -59,17 +59,17 @@ let rec unloc = function
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
   | RCases (_,rtntypopt,tml,pl) ->
       RCases (dummy_loc,
-        (option_app unloc rtntypopt),
+        (option_map unloc rtntypopt),
 	List.map (fun (tm,x) -> (unloc tm,x)) tml,
         List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
   | RLetTuple (_,nal,(na,po),b,c) ->
-      RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
+      RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c)
   | RIf (_,c,(na,po),b1,b2) ->
-      RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
+      RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2)
   | RRec (_,fk,idl,bl,tyl,bv) ->
       RRec (dummy_loc,fk,idl,
             Array.map (List.map 
-              (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty)))
+              (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty)))
               bl,
             Array.map unloc tyl,
             Array.map unloc bv)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 82f74f40..f7256026 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: topconstr.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 (*i*)
 open Pp
@@ -38,14 +38,14 @@ type aconstr =
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option *
-      (aconstr * (name * (inductive * name list) option)) list *
+      (aconstr * (name * (inductive * int * name list) option)) list *
       (identifier list * cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
-  | ACast of aconstr * cast_kind * aconstr
+  | ACast of aconstr * cast_type * aconstr
   
 let name_app f e = function
   | Name id -> let (id, e) = f id e in (e, Name id)
@@ -76,25 +76,25 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
-	| Some (ind,nal) -> 
+	| Some (ind,npar,nal) -> 
 	  let e',nal' = List.fold_right (fun na (e',nal) -> 
 	      let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in
-	  e',Some (loc,ind,nal') in
+	  e',Some (loc,ind,npar,nal') in
 	let e',na' = name_app g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
       let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
       let eqnl' = List.map (fun (idl,pat,rhs) ->
         let (idl,e) = List.fold_right fold idl ([],e) in
 	(loc,idl,pat,f e rhs)) eqnl in
-      RCases (loc,option_app (f e') rtntypopt,tml',eqnl')
+      RCases (loc,option_map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
       let e,nal = list_fold_map (name_app g) e nal in 
       let e,na = name_app g e na in
-      RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
+      RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
       let e,na = name_app g e na in
-      RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2)
-  | ACast (c,k,t) -> RCast (loc,f e c,k,f e t)
+      RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
+  | ACast (c,k,t) -> RCast (loc,f e c, k,f e t)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
   | APatVar n -> RPatVar (loc,(false,n))
@@ -182,20 +182,20 @@ let aconstr_and_vars_of_rawconstr a =
       let f (_,idl,pat,rhs) =
         found := idl@(!found);
         (idl,pat,aux rhs) in
-      ACases (option_app aux rtntypopt,
+      ACases (option_map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  option_iter
-	    (fun (_,_,nl) -> List.iter (add_name found) nl) x;
-          (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+	    (fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
+          (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
         List.map f eqnl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       add_name found na;
       List.iter (add_name found) nal;
-      ALetTuple (nal,(na,option_app aux po),aux b,aux c)
+      ALetTuple (nal,(na,option_map aux po),aux b,aux c)
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
-      AIf (aux c,(na,option_app aux po),aux b1,aux b2)
+      AIf (aux c,(na,option_map aux po),aux b1,aux b2)
   | RCast (_,c,k,t) -> ACast (aux c,k,aux t)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
@@ -289,9 +289,9 @@ let rec subst_aconstr subst bound raw =
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) -> 
 	  let a' = subst_aconstr subst bound a in
-	  let signopt' = option_app (fun ((indkn,i),nal as z) ->
+	  let signopt' = option_map (fun ((indkn,i),n,nal as z) ->
 	    let indkn' = subst_kn subst indkn in
-	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+	    if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
       and branches' = list_smartmap 
@@ -341,7 +341,7 @@ let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 (* Pattern-matching rawconstr and aconstr *)
 
 let abstract_return_type_context pi mklam tml rtno =
-  option_app (fun rtn ->
+  option_map (fun rtn ->
     let nal =
       List.flatten (List.map (fun (_,(na,t)) ->
 	match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
@@ -349,11 +349,11 @@ let abstract_return_type_context pi mklam tml rtno =
     rtno
 
 let abstract_return_type_context_rawconstr =
-  abstract_return_type_context pi3
+  abstract_return_type_context (fun (_,_,_,nal) -> nal)
     (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
 
 let abstract_return_type_context_aconstr =
-  abstract_return_type_context snd
+  abstract_return_type_context pi3
     (fun na c -> ALambda(na,AHole Evd.InternalHole,c))
 
 let rec adjust_scopes = function
@@ -524,7 +524,7 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_kind * constr_expr
+  | CCast of loc * constr_expr * cast_type * constr_expr
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -532,7 +532,7 @@ type constr_expr =
 
 
 and fixpoint_expr =
-    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
@@ -718,15 +718,15 @@ let map_constr_expr_with_binders f g e = function
             indnal (option_fold_right (name_fold g) na e))
 	  a e
       in
-      CCases (loc,option_app (f e') rtnpo,
+      CCases (loc,option_map (f e') rtnpo,
          List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
       let e'' = option_fold_right (name_fold g) ona e in
-      CLetTuple (loc,nal,(ona,option_app (f e'') po),f e b,f e' c)
+      CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c)
   | CIf (loc,c,(ona,po),b1,b2) ->
       let e' = option_fold_right (name_fold g) ona e in
-      CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
+      CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,bl,t,d) -> 
         let (e',bl') = map_local_binders f g e bl in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 2f4f667d..8305ea54 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 8624 2006-03-13 17:38:17Z msozeau $ i*)
+(*i $Id: topconstr.mli 8875 2006-05-29 19:59:11Z msozeau $ i*)
 
 (*i*)
 open Pp
@@ -34,14 +34,14 @@ type aconstr =
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option *
-      (aconstr * (name * (inductive * name list) option)) list *
+      (aconstr * (name * (inductive * int * name list) option)) list *
       (identifier list * cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
-  | ACast of aconstr * cast_kind * aconstr
+  | ACast of aconstr * cast_type * aconstr
 
 val rawconstr_of_aconstr_with_binders : loc -> 
   (identifier -> 'a -> identifier * 'a) ->
@@ -107,14 +107,14 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_kind * constr_expr
+  | CCast of loc * constr_expr * cast_type * constr_expr
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
@@ -143,7 +143,7 @@ val names_of_cases_indtype : constr_expr -> identifier list
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr
+val mkCastC : constr_expr * cast_type * constr_expr -> constr_expr
 val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * constr_expr * constr_expr -> constr_expr