diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/funind/merge.ml | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/funind/merge.ml')
-rw-r--r-- | contrib/funind/merge.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index ec456aae..9bbd165d 100644 --- a/contrib/funind/merge.ml +++ b/contrib/funind/merge.ml @@ -855,7 +855,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = [rawlist], named ident. FIXME: params et cstr_expr (arity) *) let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(identifier * rawconstr) list):inductive_expr = + (rawlist:(identifier * rawconstr) list) = let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in @@ -863,7 +863,7 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift List.map (* zeta_normalize t ? *) (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t)) rawlist in - lident , bindlist , cstr_expr , lcstor_expr + lident , bindlist , Some cstr_expr , lcstor_expr |