diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-21 00:17:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:01:21 +0100 |
| commit | 6899d3aa567436784a08af4e179c2ef1fa504a02 (patch) | |
| tree | 41ff9881c85242d2f58eb59364be3d8fa14e851c /kernel/inductive.ml | |
| parent | e7f7fc3e0582867975642fcaa7bd42140c61cd99 (diff) | |
Moving extended_rel_vect/extended_rel_list to the kernel.
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cefb5eca5..466d48715 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -292,14 +292,6 @@ let is_primitive_record (mib,_) = | Some (Some _) -> true | _ -> false -let extended_rel_list n hyps = - let rec reln l p = function - | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist |