diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 5 | ||||
| -rw-r--r-- | interp/topconstr.ml | 20 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 |
3 files changed, 17 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ecaba603d2..ceb0748fee 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1047,12 +1047,11 @@ let internalise sigma globalenv env allow_patvar lvar c = let idl = Array.map (fun (id,(n,order),bl,ty,bd) -> let intern_ro_arg f = - let idx = Option.default 0 (index_of_annot bl n) in - let before, after = list_chop idx bl in + let before, after = split_at_annot bl n in let ((ids',_,_,_) as env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern (ids', unb, tmp_scope, scopes)) in - let n' = Option.map (fun _ -> List.length before) n in + let n' = Option.map (fun _ -> List.length rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, ((ids',_,_,_),rbl) = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 5fade008cf..e9a81f09ca 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -908,17 +908,25 @@ let coerce_to_name = function (* Interpret the index of a recursion order annotation *) -let index_of_annot bl na = +let split_at_annot bl na = let names = List.map snd (names_of_local_assums bl) in match na with | None -> if names = [] then error "A fixpoint needs at least one parameter." - else None + else [], bl | Some (loc, id) -> - try Some (list_index0 (Name id) names) - with Not_found -> - user_err_loc(loc,"", - str "No parameter named " ++ Nameops.pr_id id ++ str".") + let rec aux acc = function + | LocalRawAssum (bls, k, t) as x :: rest -> + let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in + if r = [] then aux (x :: acc) rest + else + (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc), + LocalRawAssum (r, k, t) :: rest) + | LocalRawDef _ as x :: rest -> aux (x :: acc) rest + | [] -> + user_err_loc(loc,"", + str "No parameter named " ++ Nameops.pr_id id ++ str".") + in aux [] bl (* Used in correctness and interface *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 8f1fa5c3d4..a30c14966a 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -198,7 +198,7 @@ val coerce_reference_to_id : reference -> identifier val coerce_to_id : constr_expr -> identifier located val coerce_to_name : constr_expr -> name located -val index_of_annot : local_binder list -> identifier located option -> int option +val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr |