diff options
Diffstat (limited to 'contrib/recdef/recdef.ml4')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 4121580ff..e67dc1fa0 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -533,8 +533,8 @@ let (value_f:constr -> global_reference -> constr) = RLambda (d0, Name x_id, RDynamic(d0, constr_in a), RCases - (d0,(None,ref None), - [RApp(d0, RRef(d0,fterm), [RVar(d0, x_id)]),ref (Anonymous,None)], + (d0,None, + [RApp(d0, RRef(d0,fterm), [RVar(d0, x_id)]),(Anonymous,None)], [d0, [v_id], [PatCstr(d0,(ind_of_ref (Lazy.force coq_sig_ref),1), [PatVar(d0, Name v_id); |