summaryrefslogtreecommitdiff
path: root/toplevel/command.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /toplevel/command.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r--toplevel/command.ml27
1 files changed, 22 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7ff1b1b5..56a32f04 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command.ml 8689 2006-04-07 20:20:16Z herbelin $ *)
+(* $Id: command.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
open Pp
open Util
@@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
| Some comtyp ->
(* We use a cast to avoid troubles with evars in comtyp *)
(* that can only be resolved knowing com *)
- let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in
+ let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv DEFAULTcast,comtyp)) bl in
let (body,typ) = destSubCast (interp_constr sigma env b) in
{ const_entry_body = body;
const_entry_type = Some typ;
@@ -219,7 +219,7 @@ let declare_one_elimination ind =
let elim_scheme = Indrec.build_indrec env sigma ind in
let npars = mib.mind_nparams_rec in
let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in
- let kelim = mip.mind_kelim in
+ let kelim = elim_sorts (mib,mip) in
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
apropriate type *)
@@ -457,7 +457,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and sigma = Evd.empty
and env0 = Global.env()
- and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef) in
+ and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef)
+ and bl = Array.of_list (List.map (fun ((_,_,bl,_,_),_) -> bl) lnameargsardef)
+ in
(* Build the recursive context and notations for the recursive types *)
let (rec_sign,rec_impls,arityl) =
List.fold_left
@@ -502,9 +504,24 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
let recvec =
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
+ let nvrec = Array.mapi
+ (fun i (n,_) -> match n with
+ | Some n -> n
+ | None ->
+ (* Recursive argument was not given by the user :
+ We check that there is only one inductive argument *)
+ let ctx = snd (interp_context sigma env0 bl.(i)) in
+ let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in
+ (* This could be more precise (e.g. do some delta) *)
+ let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+ try (list_unique_index true lb) - 1
+ with Not_found ->
+ error "the recursive argument needs to be specified")
+ nvrec
+ in
let rec declare i fi =
let ce =
- { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *)
+ { const_entry_body = mkFix ((nvrec,i),recdecls); (* ignore rec order *)
const_entry_type = Some arrec.(i);
const_entry_opaque = false;
const_entry_boxed = boxed} in