diff options
| author | Hugo Herbelin | 2015-11-21 00:17:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 10:01:21 +0100 |
| commit | 6899d3aa567436784a08af4e179c2ef1fa504a02 (patch) | |
| tree | 41ff9881c85242d2f58eb59364be3d8fa14e851c /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ff1ed40301..0f907b0ef7 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -315,7 +315,7 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in + let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in let id = |