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 /engine | |
| 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 'engine')
| -rw-r--r-- | engine/termops.ml | 13 | ||||
| -rw-r--r-- | engine/termops.mli | 4 |
2 files changed, 0 insertions, 17 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 63baec129..db0f1e4db 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -158,19 +158,6 @@ let rel_list n m = in reln [] 1 -(* Same as [rel_list] but takes a context as argument and skips let-ins *) -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 extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) - - - let push_rel_assum (x,t) env = push_rel (x,None,t) env let push_rels_assum assums = diff --git a/engine/termops.mli b/engine/termops.mli index 94c485a26..87f74f743 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -37,13 +37,9 @@ val lookup_rel_id : Id.t -> rel_context -> int * constr option * types (** Functions that build argument lists matching a block of binders or a context. [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|] - [extended_rel_vect n ctx] extends the [ctx] context of length [m] - with [n] elements. *) val rel_vect : int -> int -> constr array val rel_list : int -> int -> constr list -val extended_rel_list : int -> rel_context -> constr list -val extended_rel_vect : int -> rel_context -> constr array (** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types |