Suppression des arguments sur les constantes, inductifs et constructeurs

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

16 files changed, 103 insertions, 150 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ee1d2ae52d..ac9777a14a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -30,7 +30,7 @@ open Evarconv
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor_path * int
+  | WrongNumargConstructor of constructor * int
   | WrongPredicateArity of constr * constr * constr
   | NeedsInversion of constr * constr
   | UnusedClause of cases_pattern list
@@ -68,7 +68,7 @@ let norec_branch_scheme env isevars cstr =
     | [] -> mkExistential isevars env in 
   crec env (List.rev cstr.cs_args)
 
-let rec_branch_scheme env isevars ((sp,j),_) recargs cstr =
+let rec_branch_scheme env isevars (sp,j) recargs cstr =
   let rec crec env (args,recargs) = 
     match args, recargs with 
       | (name,None,c as d)::rea,(ra::reca) -> 
@@ -182,16 +182,6 @@ let mssg_this_case_cannot_occur () =
   "This pattern-matching is not exhaustive."
 
 (* Utils *)
-
-let ids_of_ctxt ids =
-  try Array.to_list (Array.map destVar ids)
-  with _ -> anomaly "Context of constructor is not built from Var"
-let ctxt_of_ids ids = Array.of_list (List.map mkVar ids)
-let constructor_of_rawconstructor (cstr_sp,ids) = (cstr_sp,ctxt_of_ids ids)
-let rawconstructor_of_constructor (cstr_sp,ctxt) = (cstr_sp,ids_of_ctxt ctxt)
-let inductive_of_rawconstructor c =
-  inductive_of_constructor (constructor_of_rawconstructor c)
-
 let make_anonymous_patvars =
   list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous)) 
 
@@ -266,7 +256,7 @@ type alias_constr =
 
 type alias_builder =
   | AliasLeaf of constr
-  | AliasConstructor of alias_constr * (constructor_path * identifier list)
+  | AliasConstructor of alias_constr * constructor
 
 type history_partial_result =
   | HistoryArg of (constr * cases_pattern)
@@ -490,10 +480,10 @@ let pattern_status pats =
 (* Well-formedness tests *)
 (* Partial check on patterns *)
 
-let check_constructor loc ((_,j as cstr_sp,ids),args) mind cstrs =
+let check_constructor loc (_,j as cstr_sp) mind cstrs args =
   (* Check it is constructor of the right type *)
-  if inductive_path_of_constructor_path cstr_sp <> fst mind
-  then error_bad_constructor_loc loc (cstr_sp,ctxt_of_ids ids) mind;
+  if inductive_of_constructor cstr_sp <> mind
+  then error_bad_constructor_loc loc cstr_sp mind;
   (* Check the constructor has the right number of args *)
   let nb_args_constr = cstrs.(j-1).cs_nargs in 
   if List.length args <> nb_args_constr
@@ -503,8 +493,8 @@ let check_all_variables typ mat =
   List.iter
     (fun eqn -> match current_pattern eqn with
        | PatVar (_,id) -> ()
-       | PatCstr (loc,(cstr_sp,ids),_,_) ->
-	   error_bad_pattern_loc loc (cstr_sp,ctxt_of_ids ids) typ)
+       | PatCstr (loc,cstr_sp,_,_) ->
+	   error_bad_pattern_loc loc cstr_sp typ)
     mat
 
 let check_unused_pattern env eqn =
@@ -1048,9 +1038,9 @@ let group_equations mind current cstrs mat =
 		 let rest = {rest with tag = lower_pattern_status rest.tag} in
 		 brs.(i-1) <- (args, rest) :: brs.(i-1)
 	       done
-	   | PatCstr(loc,((ind_sp,i),ids as cstr),largs,alias) ->
+	   | PatCstr(loc,((ind_sp,i) as cstr),largs,alias) ->
 	       (* This is a regular clause *)
-	       check_constructor loc (cstr,largs) mind cstrs;
+	       check_constructor loc cstr mind cstrs largs;
 	       only_default := false;
 	       brs.(i-1) <- (largs,rest) :: brs.(i-1)) mat () in
   (brs,!only_default)
@@ -1087,8 +1077,7 @@ let build_branch current pb eqns const_info =
       DepAlias (applist (mkMutConstruct const_info.cs_cstr, params)) in
   let history = 
     push_history_pattern const_info.cs_nargs
-      (AliasConstructor
-	 (partialci, rawconstructor_of_constructor const_info.cs_cstr))
+      (AliasConstructor (partialci, const_info.cs_cstr))
       pb.history in
 
   (* We find matching clauses *)
@@ -1350,7 +1339,7 @@ let coerce_row typing_fun isevars env cstropt tomatch =
   let typ = body_of_type j.uj_type in
   let t = match cstropt with
       | Some (cloc,(cstr,_ as c)) ->
-	  (let tyi = inductive_of_rawconstructor c in
+	  (let tyi = inductive_of_constructor c in
 	   try 
 	     let indtyp = inh_coerce_to_ind isevars env typ tyi in
 	     IsInd (typ,find_rectype env (evars_of isevars) typ)
@@ -1358,8 +1347,7 @@ let coerce_row typing_fun isevars env cstropt tomatch =
 	     (* 2 cases : Not the right inductive or not an inductive at all *)
 	     try
 	       let mind,_ = find_mrectype env (evars_of isevars) typ in
-	       error_bad_constructor_loc cloc
-		 (constructor_of_rawconstructor c) mind
+	       error_bad_constructor_loc cloc c mind
 	     with Induc ->
 	       error_case_not_inductive_loc
 		 (loc_of_rawconstr tomatch) CCI env (evars_of isevars) j)
@@ -1381,7 +1369,7 @@ let coerce_to_indtype typing_fun isevars env matx tomatchl =
 let build_expected_arity env isevars isdep tomatchl =
   let cook n = function
     | _,IsInd (_,IndType(indf,_)) ->
-	let indf' = lift_inductive_family n indf in
+        let indf' = lift_inductive_family n indf in
 	Some (build_dependent_inductive indf', fst (get_arity indf'))
     | _,NotInd _ -> None
   in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 7e5fda9037..e44bda7d21 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -21,7 +21,7 @@ open Evarutil
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor_path * int
+  | WrongNumargConstructor of constructor * int
   | WrongPredicateArity of constr * constr * constr
   | NeedsInversion of constr * constr
   | UnusedClause of cases_pattern list
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 77370dedc6..c4f5b13a42 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -34,8 +34,7 @@ open Esubst
  *  FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under
  *          the substitution S, and then applied to args. Here again,
  *          weak reduction.
- *  CONSTR(n,(sp,i),vars,args) is the n-th constructor of the i-th
- *          inductive type sp.
+ *  CONSTR(c,args) is the constructor [c] applied to [args].
  *
  * Note that any term has not an equivalent in cbv_value: for example,
  * a product (x:A)B must be in normal form because only VAL may
@@ -49,7 +48,7 @@ type cbv_value =
   | LAM of name * constr * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value list
   | COFIXP of cofixpoint * cbv_value subs * cbv_value list
-  | CONSTR of int * inductive_path * cbv_value array * cbv_value list
+  | CONSTR of constructor * cbv_value list
 
 (* les vars pourraient etre des constr,
    cela permet de retarder les lift: utile ?? *) 
@@ -64,9 +63,8 @@ let rec shift_value n = function
       FIXP (fix,subs_shft (n,s), List.map (shift_value n) args)
   | COFIXP (cofix,s,args) ->
       COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args)
-  | CONSTR (i,spi,vars,args) ->
-      CONSTR (i, spi, Array.map (shift_value n) vars,
-              List.map (shift_value n) args)
+  | CONSTR (c,args) ->
+      CONSTR (c, List.map (shift_value n) args)
 	
 
 (* Contracts a fixpoint: given a fixpoint and a substitution,
@@ -142,7 +140,7 @@ let red_allowed_ref flags stack = function
   | FarRelBinding _ -> red_allowed flags stack fDELTA
   | VarBinding id -> red_allowed flags stack (fVAR id)
   | EvarBinding _ -> red_allowed flags stack fEVAR
-  | ConstBinding (sp,_) -> red_allowed flags stack (fCONST sp)
+  | ConstBinding sp -> red_allowed flags stack (fCONST sp)
 
 (* Transfer application lists from a value to the stack
  * useful because fixpoints may be totally applied in several times
@@ -151,7 +149,7 @@ let strip_appl head stack =
   match head with
     | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack)
     | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack)
-    | CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack)
+    | CONSTR (c,app) -> (CONSTR(c,[]), stack_app app stack)
     | _ -> (head, stack)
 
 
@@ -232,9 +230,8 @@ let rec norm_head info env t stack =
 
   | IsVar id -> norm_head_ref 0 info env stack (VarBinding id)
 
-  | IsConst (sp,vars) ->
-      let normt = (sp,Array.map (cbv_norm_term info env) vars) in
-      norm_head_ref 0 info env stack (ConstBinding normt)
+  | IsConst sp ->
+      norm_head_ref 0 info env stack (ConstBinding sp)
 
   | IsEvar (ev,args) ->
       let evar = (ev, Array.map (cbv_norm_term info env) args) in
@@ -262,13 +259,10 @@ let rec norm_head info env t stack =
   | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack)
   | IsFix fix -> (FIXP(fix,env,[]), stack)
   | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack)
-  | IsMutConstruct ((spi,i),vars) ->
-      (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack)
+  | IsMutConstruct c -> (CONSTR(c, []), stack)
 
   (* neutral cases *)
-  | (IsSort _ | IsMeta _) -> (VAL(0, t), stack)
-  | IsMutInd (sp,vars) -> 
-      (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack)
+  | (IsSort _ | IsMeta _ | IsMutInd _) -> (VAL(0, t), stack)
   | IsProd (x,t,c) -> 
       (VAL(0, mkProd (x, cbv_norm_term info env t,
 		      cbv_norm_term info (subs_lift env) c)),
@@ -317,17 +311,13 @@ and cbv_stack_term info stack env t =
 
     (* constructor in a Case -> IOTA
        (use red_under because we know there is a Case) *)
-    | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,(arity,_),env,stk)))
+    | (CONSTR((sp,n),_), APP(args,CASE(_,br,(arity,_),env,stk)))
             when red_under (info_flags info) fIOTA ->
-(*
-	let ncargs = arity.(n-1) in
-	let real_args = list_lastn ncargs args in
-*)
 	let real_args = snd (list_chop arity args) in
         cbv_stack_term info (stack_app real_args stk) env br.(n-1)
          
     (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
-    | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk))
+    | (CONSTR((_,n),_), CASE(_,br,_,env,stk))
                   when red_under (info_flags info) fIOTA ->
                     cbv_stack_term info stk env br.(n-1)
 
@@ -335,7 +325,7 @@ and cbv_stack_term info stack env t =
     | (head, TOP) -> head
     | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl) 
     | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) 
-    | (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl)
+    | (CONSTR(c,_), APP(appl,TOP)) -> CONSTR(c,appl)
 
     (* definitely a value *)
     | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
@@ -390,9 +380,9 @@ and cbv_norm_value info = function (* reduction under binders *)
 		   Array.map (cbv_norm_term info 
 				(subs_liftn (Array.length lty) env)) bds)))
         (List.map (cbv_norm_value info) args)
-  | CONSTR (n,spi,vars,args) ->
+  | CONSTR (c,args) ->
       applistc
-        (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars))
+        (mkMutConstruct c)
         (List.map (cbv_norm_value info) args)
 
 (* with profiling *)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 7271a3c0be..d787111370 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -33,7 +33,7 @@ type cbv_value =
   | LAM of name * constr * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value list
   | COFIXP of cofixpoint * cbv_value subs * cbv_value list
-  | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
+  | CONSTR of constructor * cbv_value list
 
 val shift_value : int -> cbv_value -> cbv_value
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 556dbd3341..5a88e62dca 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -22,24 +22,24 @@ open Rawterm
 (* usage qque peu general: utilise aussi dans record *)
 
 type cte_typ = 
-  | NAM_Section_Variable of variable_path
-  | NAM_Constant of constant_path
-  | NAM_Inductive of inductive_path
-  | NAM_Constructor of constructor_path
+  | NAM_Section_Variable of variable
+  | NAM_Constant of constant
+  | NAM_Inductive of inductive
+  | NAM_Constructor of constructor
 
 let cte_of_constr c = match kind_of_term c with
-  | IsConst (sp,_) -> ConstRef sp
-  | IsMutInd (ind_sp,_) -> IndRef ind_sp
-  | IsMutConstruct (cstr_cp,_) -> ConstructRef cstr_cp
+  | IsConst sp -> ConstRef sp
+  | IsMutInd ind_sp -> IndRef ind_sp
+  | IsMutConstruct cstr_cp -> ConstructRef cstr_cp
   | IsVar id -> VarRef (Declare.find_section_variable id)
   |  _ -> raise Not_found
 
 type cl_typ = 
   | CL_SORT 
   | CL_FUN
-  | CL_SECVAR of variable_path
-  | CL_CONST of constant_path
-  | CL_IND of inductive_path
+  | CL_SECVAR of variable
+  | CL_CONST of constant
+  | CL_IND of inductive
 
 type cl_info_typ = {
   cl_strength : strength;
@@ -203,8 +203,8 @@ let _ =
 let constructor_at_head t = 
   let rec aux t' = match kind_of_term t' with
     | IsVar id -> CL_SECVAR (find_section_variable id),0
-    | IsConst (sp,_) -> CL_CONST sp,0
-    | IsMutInd (ind_sp,_) -> CL_IND ind_sp,0
+    | IsConst sp -> CL_CONST sp,0
+    | IsMutInd ind_sp -> CL_IND ind_sp,0
     | IsProd (_,_,c) -> CL_FUN,0
     | IsLetIn (_,_,_,c) -> aux c
     | IsSort _ -> CL_SORT,0
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 4b52616476..019644e20a 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -20,9 +20,9 @@ open Declare
 type cl_typ = 
   | CL_SORT 
   | CL_FUN 
-  | CL_SECVAR of variable_path
-  | CL_CONST of constant_path
-  | CL_IND of inductive_path
+  | CL_SECVAR of variable
+  | CL_CONST of constant
+  | CL_IND of inductive
 
 (* This is the type of infos for declared classes *)
 type cl_info_typ = {
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2aada52ee2..b4df53b8a8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -46,10 +46,10 @@ let occur_rel p env id =
 let occur_id env id0 c =
   let rec occur n c = match kind_of_term c with
     | IsVar id when  id=id0 -> raise Occur
-    | IsConst (sp, _) when basename sp = id0 -> raise Occur
-    | IsMutInd (ind_sp, _)
+    | IsConst sp when basename sp = id0 -> raise Occur
+    | IsMutInd ind_sp
 	when basename (path_of_inductive_path ind_sp) = id0 -> raise Occur
-    | IsMutConstruct (cstr_sp, _) 
+    | IsMutConstruct cstr_sp
 	when basename (path_of_constructor_path cstr_sp) = id0 -> raise Occur
     | IsRel p when p>n & occur_rel (p-n) env id0 -> raise Occur
     | _ -> iter_constr_with_binders succ occur n c
@@ -99,18 +99,18 @@ let used_of = global_vars_and_consts
 (* Tools for printing of Cases                                              *)
 
 let encode_inductive ref =
-  let (indsp,_ as ind) =
+  let indsp =
       match kind_of_term (constr_of_reference Evd.empty (Global.env()) ref)with
-        | IsMutInd (indsp,args) -> (indsp,args)
+        | IsMutInd indsp -> indsp
 	| _ -> errorlabstrm "indsp_of_id" 
-	    [< 'sTR ((Global.string_of_global ref)^" is not an inductive type") >]
-  in
-  let mis = Global.lookup_mind_specif ind in
+	    [< 'sTR ((Global.string_of_global ref)^
+                      " is not an inductive type") >] in
+  let mis = Global.lookup_mind_specif indsp in
   let constr_lengths = Array.map List.length (mis_recarg mis) in
   (indsp,constr_lengths)
 
 let constr_nargs indsp =
-  let mis = Global.lookup_mind_specif (indsp,[||] (* ?? *)) in
+  let mis = Global.lookup_mind_specif indsp in
   let nparams = mis_nparams mis in
   Array.map (fun t -> List.length (fst (decompose_prod_assum t)) - nparams)
     (mis_nf_lc mis)
@@ -138,7 +138,7 @@ module PrintingCasesMake =
      val title : string
   end) ->
   struct
-    type t = inductive_path * int array
+    type t = inductive * int array
     let encode = encode_inductive
     let check (_,lc) =
       if not (Test.test lc) then 
@@ -292,15 +292,14 @@ let rec detype avoid env t =
     | IsLetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c
     | IsApp (f,args) ->
 	RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args)
-    | IsConst (sp,cl) ->
-	detype_reference avoid env (ConstRef sp) cl
+    | IsConst sp -> RRef (dummy_loc, ConstRef sp)
     | IsEvar (ev,cl) ->
 	let f = REvar (dummy_loc, ev) in
 	RApp (dummy_loc, f, List.map (detype avoid env) (Array.to_list cl))
-    | IsMutInd (ind_sp,cl) ->
-	detype_reference avoid env (IndRef ind_sp) cl
-    | IsMutConstruct (cstr_sp,cl) ->
-	detype_reference avoid env (ConstructRef cstr_sp) cl
+    | IsMutInd ind_sp ->
+	RRef (dummy_loc, IndRef ind_sp)
+    | IsMutConstruct cstr_sp ->
+	RRef (dummy_loc, ConstructRef cstr_sp)
     | IsMutCase (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
 	let tomatch = detype avoid env c in
@@ -312,8 +311,7 @@ let rec detype avoid env t =
 	  else 
 	    Some (detype avoid env p) in
 	let constructs = 
-	  Array.init (Array.length considl)
-	    (fun i -> ((indsp,i+1),[] (* on triche *))) in
+	  Array.init (Array.length considl) (fun i -> (indsp,i+1)) in
 	let eqnv =
 	  array_map3 (detype_eqn avoid env) constructs consnargsl bl in
 	let eqnl = Array.to_list eqnv in
@@ -330,20 +328,6 @@ let rec detype avoid env t =
     | IsFix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef
     | IsCoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef
 
-and detype_reference avoid env ref args =
-  let args = 
-    try Array.to_list (extract_instance ref args)
-    with Not_found -> (* May happen in debugger *)
-      if Array.length args = 0 then []
-      else
-	let m = "<<Cannot split "^(string_of_int (Array.length args))^
-		" arguments>>" in
-	(mkVar (id_of_string m))::(Array.to_list args)
-  in
-  let f = RRef (dummy_loc, ref) in
-  if args = [] then f
-  else RApp (dummy_loc, f, List.map (detype avoid env) args)
-
 and detype_fix avoid env fixkind (names,tys,bodies) =
   let lfi = Array.map (fun id -> next_name_away id avoid) names in
   let def_avoid = Array.to_list lfi@avoid in
@@ -353,7 +337,7 @@ and detype_fix avoid env fixkind (names,tys,bodies) =
        Array.map (detype def_avoid def_env) bodies)
 
 
-and detype_eqn avoid env constr_id construct_nargs branch =
+and detype_eqn avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
     if not (force_wildcard ()) or (dependent (mkRel 1) b) then
       let id = next_name_away_with_default "x" x avoid in
@@ -364,7 +348,7 @@ and detype_eqn avoid env constr_id construct_nargs branch =
   let rec buildrec ids patlist avoid env n b =
     if n=0 then
       (dummy_loc, ids, 
-       [PatCstr(dummy_loc, constr_id, List.rev patlist,Anonymous)],
+       [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
        detype avoid env b)
     else
       match kind_of_term b with
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f40ad4dc00..e221e49450 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -241,14 +241,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (let c = nf_evar (evars_of isevars) c1 in
 	     evar_conv_x (push_rel_assum (n,c) env) isevars pbty c'1 c'2)
 
-	| IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
+	| IsMutInd sp1, IsMutInd sp2 ->
 	    sp1=sp2
-	    & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
             & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
              
-	| IsMutConstruct (sp1,cl1), IsMutConstruct (sp2,cl2) ->
+	| IsMutConstruct sp1, IsMutConstruct sp2 ->
 	    sp1=sp2
-            & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
             & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
 
 	| IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) ->
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 66125bfeb0..54e67e401c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -46,9 +46,9 @@ let rec occur_meta_pattern = function
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
 type constr_label =
-  | ConstNode of section_path
-  | IndNode of inductive_path
-  | CstrNode of constructor_path
+  | ConstNode of constant
+  | IndNode of inductive
+  | CstrNode of constructor
   | VarNode of identifier
 
 exception BoundPattern;;
@@ -74,9 +74,9 @@ let rec head_pattern_bound t =
     | PCoFix _ -> anomaly "head_pattern_bound: not a type"
 
 let head_of_constr_reference c = match kind_of_term c with
-  | IsConst (sp,_) -> ConstNode sp
-  | IsMutConstruct (sp,_) -> CstrNode sp
-  | IsMutInd (sp,_) -> IndNode sp
+  | IsConst sp -> ConstNode sp
+  | IsMutConstruct sp -> CstrNode sp
+  | IsMutInd sp -> IndNode sp
   | IsVar id -> VarNode id
   | _ -> anomaly "Not a rigid reference"
 
@@ -311,9 +311,9 @@ let rec pattern_of_constr t =
     | IsProd (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
     | IsLambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
     | IsApp (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
-    | IsConst (sp,ctxt)         -> pattern_of_ref (ConstRef sp) ctxt
-    | IsMutInd (sp,ctxt)        -> pattern_of_ref (IndRef sp) ctxt
-    | IsMutConstruct (sp,ctxt) -> pattern_of_ref (ConstructRef sp) ctxt
+    | IsConst sp         -> PRef (ConstRef sp)
+    | IsMutInd sp        -> PRef (IndRef sp)
+    | IsMutConstruct sp -> PRef (ConstructRef sp)
     | IsEvar (n,ctxt) ->
 	if ctxt = [||] then PEvar n
 	else PApp (PEvar n, Array.map pattern_of_constr ctxt)
@@ -323,8 +323,3 @@ let rec pattern_of_constr t =
     | IsFix f -> PFix f
     | IsCoFix _ ->
 	error "pattern_of_constr: (co)fix currently not supported"
-
-and pattern_of_ref ref inst =
-  let args = Declare.extract_instance ref inst in
-  let f = PRef ref in
-  if args = [||] then f else PApp (f, Array.map pattern_of_constr args)
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 91dd32ba3d..42b6808204 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -34,9 +34,9 @@ type constr_pattern =
 val occur_meta_pattern : constr_pattern -> bool
 
 type constr_label =
-  | ConstNode of section_path
-  | IndNode of inductive_path
-  | CstrNode of constructor_path
+  | ConstNode of constant
+  | IndNode of inductive
+  | CstrNode of constructor
   | VarNode of identifier
 
 val label_of_ref : global_reference -> constr_label
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cb9e0abd6d..2cb322bea8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -221,7 +221,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
       let hyps = (Evd.map (evars_of isevars) ev).evar_hyps in
       let args = instance_from_named_context hyps in
-      let c = mkEvar (ev, Array.of_list args) in
+      let c = mkEvar (ev, args) in
       let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
       inh_conv_coerce_to_tycon loc env isevars j tycon
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index a46a3f8b5b..c8c91a945a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -23,17 +23,16 @@ type loc = int * int
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
 type cases_pattern =
   | PatVar of loc * name
-  | PatCstr of
-      loc * (constructor_path * identifier list) * cases_pattern list * name
+  | PatCstr of loc * constructor * cases_pattern list * name
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
 type 'ctxt reference =
-  | RConst of section_path * 'ctxt
-  | RInd of inductive_path * 'ctxt
-  | RConstruct of constructor_path * 'ctxt
+  | RConst of constant * 'ctxt
+  | RInd of inductive * 'ctxt
+  | RConstruct of constructor * 'ctxt
   | RVar of identifier
   | REVar of int * 'ctxt
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 22492a6cc6..336b3ffa1e 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -22,17 +22,16 @@ type loc = int * int
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
 type cases_pattern =
   | PatVar of loc * name
-  | PatCstr of
-      loc * (constructor_path * identifier list) * cases_pattern list * name
+  | PatCstr of loc * constructor * cases_pattern list * name
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
 type 'ctxt reference =
-  | RConst of section_path * 'ctxt
-  | RInd of inductive_path * 'ctxt
-  | RConstruct of constructor_path * 'ctxt
+  | RConst of constant * 'ctxt
+  | RInd of inductive * 'ctxt
+  | RConstruct of constructor * 'ctxt
   | RVar of identifier
   | REVar of int * 'ctxt
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cabdaa62c7..c3c2954287 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -34,7 +34,7 @@ type struc_typ = {
   s_PARAM : int;
   s_PROJ : section_path option list }
 
-let sTRUCS = (ref [] : (inductive_path * struc_typ) list ref)
+let sTRUCS = (ref [] : (inductive * struc_typ) list ref)
 
 let add_new_struc1 x = sTRUCS:=x::(!sTRUCS)
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 25e024a6cf..3684bb2286 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -29,11 +29,11 @@ type struc_typ = {
   s_PROJ : section_path option list }
 
 val add_new_struc : 
-  inductive_path * identifier * int * section_path option list -> unit
+  inductive * identifier * int * section_path option list -> unit
 
 (* [find_structure isp] returns the infos associated to inductive path
    [isp] if it corresponds to a structure, otherwise fails with [Not_found] *)
-val find_structure : inductive_path -> struc_typ
+val find_structure : inductive -> struc_typ
 
 type obj_typ = {
   o_DEF : constr;
@@ -47,8 +47,8 @@ val add_new_objdef :
   Term.constr list * Term.constr list -> unit
 
 
-val inStruc : inductive_path * struc_typ -> obj
-val outStruc : obj -> inductive_path * struc_typ
+val inStruc : inductive * struc_typ -> obj
+val outStruc : obj -> inductive * struc_typ
 val inObjDef1 : section_path -> obj
 val outObjDef1 : obj -> section_path
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index cc907ac7ab..7d1564a8c0 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -24,7 +24,7 @@ exception Redelimination
 
 let check_transparency env ref =
   match ref with
-      EvalConst (sp,_) -> Opaque.is_evaluable env (EvalConstRef sp)
+      EvalConst sp -> Opaque.is_evaluable env (EvalConstRef sp)
     | EvalVar id -> Opaque.is_evaluable env (EvalVarRef id)
     | _ -> false
 
@@ -128,8 +128,8 @@ let invert_name labs l na0 env sigma ref = function
 	let refi = match ref with
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
-	  | EvalConst (sp,args) ->
-	      Some (EvalConst (make_path (dirpath sp) id CCI, args)) in
+	  | EvalConst sp ->
+	      Some (EvalConst (make_path (dirpath sp) id CCI)) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -298,9 +298,9 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
   let subbodies = list_tabulate make_Fi nbodies in
   substl subbodies bodies.(bodynum)
 
-let reduce_mind_case_use_function (sp,args) env mia =
+let reduce_mind_case_use_function sp env mia =
   match kind_of_term mia.mconstr with 
-    | IsMutConstruct(ind_sp,i as cstr_sp, args) ->
+    | IsMutConstruct(ind_sp,i as cstr_sp) ->
 	let real_cargs = snd (list_chop (fst mia.mci) mia.mcargs) in
 	applist (mia.mlf.(i-1), real_cargs)
     | IsCoFix (_,(names,_,_) as cofix) ->
@@ -308,9 +308,9 @@ let reduce_mind_case_use_function (sp,args) env mia =
 	  match names.(i) with 
 	    | Name id ->
 		let sp = make_path (dirpath sp) id (kind_of_path sp) in
-		(match constant_opt_value env (sp,args) with
+		(match constant_opt_value env sp with
 		  | None -> None
-		  | Some _ -> Some (mkConst (sp,args)))
+		  | Some _ -> Some (mkConst sp))
 	    | Anonymous -> None in 
 	let cofix_def = contract_cofix_use_function build_fix_name cofix in
 	mkMutCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
@@ -320,8 +320,8 @@ let special_red_case env whfun (ci, p, c, lf)  =
   let rec redrec s = 
     let (constr, cargs) = whfun s in 
     match kind_of_term constr with 
-      | IsConst (sp,args as cst) -> 
-          (if not (Opaque.is_evaluable env (EvalConstRef sp)) then
+      | IsConst cst -> 
+          (if not (Opaque.is_evaluable env (EvalConstRef cst)) then
             raise Redelimination;
 	  let gvalue = constant_value env cst in
 	  if reducible_mind_case gvalue then
@@ -528,14 +528,14 @@ let nf env sigma c = strong whd_nf env sigma c
  * ol is the occurence list to find. *)
 let rec substlin env name n ol c =
   match kind_of_term c with
-    | IsConst (sp,_ as const) when EvalConstRef sp = name ->
+    | IsConst const when EvalConstRef const = name ->
         if List.hd ol = n then
           try 
 	    (n+1, List.tl ol, constant_value env const)
           with
 	      NotEvaluableConst _ ->
 		errorlabstrm "substlin"
-		  [< pr_sp sp; 'sTR " is not a defined constant" >]
+		  [< pr_sp const; 'sTR " is not a defined constant" >]
         else 
 	  ((n+1), ol, c)