diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2057eb5b2..0be6b9dc6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -793,7 +793,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 diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 4d4e3f88a..d82c04e07 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -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 diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 073f9ba0b..4e2017f44 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -114,7 +114,7 @@ type 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 |