diff options
| author | herbelin | 2009-11-11 16:03:06 +0000 |
|---|---|---|
| committer | herbelin | 2009-11-11 16:03:06 +0000 |
| commit | e46a343090514c1340d4e5b97384b55b42c9c166 (patch) | |
| tree | afe12355bdb7e823b5881b4a89d54b6753684001 /plugins/funind | |
| parent | d27a272511939ba80f1b3658be064268ec9ba55e (diff) | |
Added support for multiple where-clauses in Inductive and co (see wish #2163).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/rawterm_to_relation.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 77389681b3..bd3f7e8ec8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -527,7 +527,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) in - (name,annot,args,types,body),(None:Vernacexpr.decl_notation option) + (name,annot,args,types,body),([]:Vernacexpr.decl_notation list) | (name,None,args,types,body),recdef -> let names = (Topconstr.names_of_local_assums args) in if is_one_rec recdef && List.length names > 1 then @@ -537,7 +537,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp else let loc, na = List.hd names in (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body), - (None:Vernacexpr.decl_notation option) + ([]:Vernacexpr.decl_notation list) | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> error ("Cannot use mutual definition with well-founded recursion or measure") diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 04e36d945d..c69e04b938 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -904,7 +904,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,None)] in + let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations false mie impls) diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml index 752e546c89..f69dd2fe68 100644 --- a/plugins/funind/rawterm_to_relation.ml +++ b/plugins/funind/rawterm_to_relation.ml @@ -1338,7 +1338,7 @@ let do_build_inductive ((dummy_loc,relnames.(i)), rel_params, Some rel_arities.(i), - ext_rel_constructors),None + ext_rel_constructors),[] in let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in let rel_inds = Array.to_list ext_rel_constructors in |