diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/indfun.ml | 6 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 14 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 3 |
3 files changed, 16 insertions, 7 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 2fcdd3a75d..d7c045a60d 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -317,7 +317,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = (Topconstr.names_of_local_assums args) in let annot = - try Util.list_index (Name id) names - 1, Topconstr.CStructRec + try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) in (name,annot,args,types,body),(None:Vernacexpr.decl_notation) @@ -328,7 +328,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = (Util.dummy_loc,"GenFixpoint", Pp.str "the recursive argument needs to be specified") else - (name,(0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation) + (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation) | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> error ("Cannot use mutual definition with well-founded recursion") @@ -417,7 +417,7 @@ let make_graph (id:identifier) = ) in let rec_id = - match List.nth nal n with |(_,Name id) -> id | _ -> anomaly "" + match List.nth nal (out_some n) with |(_,Name id) -> id | _ -> anomaly "" in (id, Some (Struct rec_id),bl,t,b) ) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index da87086e29..a78c35d1dd 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -298,9 +298,11 @@ let rec decompose_last = function let make_fix_struct (n,bl) = let names = names_of_local_assums bl in let nn = List.length names in - if nn = 1 then ctv_ID_OPT_NONE - else if n < nn then xlate_id_opt(List.nth names n) - else xlate_error "unexpected result of parsing for Fixpoint";; + if nn = 1 || n = None then ctv_ID_OPT_NONE + else + let n = out_some n in + if n < nn then xlate_id_opt(List.nth names n) + else xlate_error "unexpected result of parsing for Fixpoint";; let rec xlate_binder = function @@ -417,7 +419,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CFix (_, (_, id), lm::lmi) -> let strip_mutrec (fid, (n, ro), bl, arf, ardef) = let (struct_arg,bl,arf,ardef) = + (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *) + (* By the way, how could [bl = []] happen in V8 syntax ? *) if bl = [] then + let n = out_some n in let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef) else (make_fix_struct (n, bl),bl,arf,ardef) in @@ -1875,7 +1880,10 @@ let rec xlate_vernac = | VernacFixpoint ((lm :: lmi),boxed) -> let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) = let (struct_arg,bl,arf,ardef) = + (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *) + (* By the way, how could [bl = []] happen in V8 syntax ? *) if bl = [] then + let n = out_some n in let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef) else (make_fix_struct (n, bl),bl,arf,ardef) in diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 1b92c69110..727ba82ae3 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -200,6 +200,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl) | CWfRec r -> + let n = out_some n in let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ Ppconstr.pr_binders bl ++ str " : " ++ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ @@ -279,7 +280,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env0 lrecnames recdef arityl nv in - let nvrec' = Array.map fst nvrec in(* ignore rec order *) + let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *) let declare arrec defrec = let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in |